Home | Intuitionistic Logic Explorer Theorem List (p. 18 of 105) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hbsb2a 1701 | Special case of a bound-variable hypothesis builder for substitution. (Contributed by NM, 2-Feb-2007.) |
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | hbsb2e 1702 | Special case of a bound-variable hypothesis builder for substitution. (Contributed by NM, 2-Feb-2007.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]∃𝑦𝜑) | ||
Theorem | hbsb3 1703 | If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | nfs1 1704 | If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
Theorem | sbcof2 1705 | Version of sbco 1856 where 𝑥 is not free in 𝜑. (Contributed by Jim Kingdon, 28-Dec-2017.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | spimv 1706* | A version of spim 1640 with a distinct variable requirement instead of a bound variable hypothesis. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | aev 1707* | A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-16 1709. (Contributed by NM, 8-Nov-2006.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑤 = 𝑣) | ||
Theorem | ax16 1708* |
Theorem showing that ax-16 1709 is redundant if ax-17 1433 is included in the
axiom system. The important part of the proof is provided by aev 1707.
See ax16ALT 1753 for an alternate proof that does not require ax-10 1410 or ax-12 1416. This theorem should not be referenced in any proof. Instead, use ax-16 1709 below so that theorems needing ax-16 1709 can be more easily identified. (Contributed by NM, 8-Nov-2006.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Axiom | ax-16 1709* |
Axiom of Distinct Variables. The only axiom of predicate calculus
requiring that variables be distinct (if we consider ax-17 1433 to be a
metatheorem and not an axiom). Axiom scheme C16' in [Megill] p. 448 (p.
16 of the preprint). It apparently does not otherwise appear in the
literature but is easily proved from textbook predicate calculus by
cases. It is a somewhat bizarre axiom since the antecedent is always
false in set theory, but nonetheless it is technically necessary as you
can see from its uses.
This axiom is redundant if we include ax-17 1433; see theorem ax16 1708. This axiom is obsolete and should no longer be used. It is proved above as theorem ax16 1708. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | dveeq2 1710* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | dveeq2or 1711* | Quantifier introduction when one pair of variables is distinct. Like dveeq2 1710 but connecting ∀𝑥𝑥 = 𝑦 by a disjunction rather than negation and implication makes the theorem stronger in intuitionistic logic. (Contributed by Jim Kingdon, 1-Feb-2018.) |
⊢ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥 𝑧 = 𝑦) | ||
Theorem | dvelimfALT2 1712* | Proof of dvelimf 1905 using dveeq2 1710 (shown as the last hypothesis) instead of ax-12 1416. This shows that ax-12 1416 could be replaced by dveeq2 1710 (the last hypothesis). (Contributed by Andrew Salmon, 21-Jul-2011.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑧𝜓) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | nd5 1713* | A lemma for proving conditionless ZFC axioms. (Contributed by NM, 8-Jan-2002.) |
⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | exlimdv 1714* | Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒)) | ||
Theorem | ax11v2 1715* | Recovery of ax11o 1717 from ax11v 1722 without using ax-11 1411. The hypothesis is even weaker than ax11v 1722, with 𝑧 both distinct from 𝑥 and not occurring in 𝜑. Thus the hypothesis provides an alternate axiom that can be used in place of ax11o 1717. (Contributed by NM, 2-Feb-2007.) |
⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | ax11a2 1716* | Derive ax-11o 1718 from a hypothesis in the form of ax-11 1411. The hypothesis is even weaker than ax-11 1411, with 𝑧 both distinct from 𝑥 and not occurring in 𝜑. Thus the hypothesis provides an alternate axiom that can be used in place of ax11o 1717. (Contributed by NM, 2-Feb-2007.) |
⊢ (𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | ax11o 1717 |
Derivation of set.mm's original ax-11o 1718 from the shorter ax-11 1411 that
has replaced it.
An open problem is whether this theorem can be proved without relying on ax-16 1709 or ax-17 1433. Normally, ax11o 1717 should be used rather than ax-11o 1718, except by theorems specifically studying the latter's properties. (Contributed by NM, 3-Feb-2007.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Axiom | ax-11o 1718 |
Axiom ax-11o 1718 ("o" for "old") was the
original version of ax-11 1411,
before it was discovered (in Jan. 2007) that the shorter ax-11 1411 could
replace it. It appears as Axiom scheme C15' in [Megill] p. 448 (p. 16 of
the preprint). It is based on Lemma 16 of [Tarski] p. 70 and Axiom C8 of
[Monk2] p. 105, from which it can be proved
by cases. To understand this
theorem more easily, think of "¬ ∀𝑥𝑥 = 𝑦 →..." as informally
meaning "if 𝑥 and 𝑦 are distinct variables
then..." The
antecedent becomes false if the same variable is substituted for 𝑥 and
𝑦, ensuring the theorem is sound
whenever this is the case. In some
later theorems, we call an antecedent of the form ¬
∀𝑥𝑥 = 𝑦 a
"distinctor."
This axiom is redundant, as shown by theorem ax11o 1717. This axiom is obsolete and should no longer be used. It is proved above as theorem ax11o 1717. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) | ||
Theorem | albidv 1719* | Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) | ||
Theorem | exbidv 1720* | Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | ||
Theorem | ax11b 1721 | A bidirectional version of ax-11o 1718. (Contributed by NM, 30-Jun-2006.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | ax11v 1722* | This is a version of ax-11o 1718 when the variables are distinct. Axiom (C8) of [Monk2] p. 105. (Contributed by NM, 5-Aug-1993.) (Revised by Jim Kingdon, 15-Dec-2017.) |
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | ax11ev 1723* | Analogue to ax11v 1722 for existential quantification. (Contributed by Jim Kingdon, 9-Jan-2018.) |
⊢ (𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → 𝜑)) | ||
Theorem | equs5 1724 | Lemma used in proofs of substitution properties. (Contributed by NM, 5-Aug-1993.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | equs5or 1725 | Lemma used in proofs of substitution properties. Like equs5 1724 but, in intuitionistic logic, replacing negation and implication with disjunction makes this a stronger result. (Contributed by Jim Kingdon, 2-Feb-2018.) |
⊢ (∀𝑥 𝑥 = 𝑦 ∨ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | sb3 1726 | One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 5-Aug-1993.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) | ||
Theorem | sb4 1727 | One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 5-Aug-1993.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | sb4or 1728 | One direction of a simplified definition of substitution when variables are distinct. Similar to sb4 1727 but stronger in intuitionistic logic. (Contributed by Jim Kingdon, 2-Feb-2018.) |
⊢ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | sb4b 1729 | Simplified definition of substitution when variables are distinct. (Contributed by NM, 27-May-1997.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | sb4bor 1730 | Simplified definition of substitution when variables are distinct, expressed via disjunction. (Contributed by Jim Kingdon, 18-Mar-2018.) |
⊢ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | hbsb2 1731 | Bound-variable hypothesis builder for substitution. (Contributed by NM, 5-Aug-1993.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)) | ||
Theorem | nfsb2or 1732 | Bound-variable hypothesis builder for substitution. Similar to hbsb2 1731 but in intuitionistic logic a disjunction is stronger than an implication. (Contributed by Jim Kingdon, 2-Feb-2018.) |
⊢ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | sbequilem 1733 | Propositional logic lemma used in the sbequi 1734 proof. (Contributed by Jim Kingdon, 1-Feb-2018.) |
⊢ (𝜑 ∨ (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜏 ∨ (𝜓 → (𝜃 → 𝜂))) ⇒ ⊢ (𝜑 ∨ (𝜏 ∨ (𝜓 → (𝜒 → 𝜂)))) | ||
Theorem | sbequi 1734 | An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.) (Proof modified by Jim Kingdon, 1-Feb-2018.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) | ||
Theorem | sbequ 1735 | An equality theorem for substitution. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) | ||
Theorem | drsb2 1736 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) | ||
Theorem | spsbe 1737 | A specialization theorem, mostly the same as Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 29-Dec-2017.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥𝜑) | ||
Theorem | spsbim 1738 | Specialization of implication. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 21-Jan-2018.) |
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | spsbbi 1739 | Specialization of biconditional. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 21-Jan-2018.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbbid 1740 | Deduction substituting both sides of a biconditional. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒)) | ||
Theorem | sbequ8 1741 | Elimination of equality from antecedent after substitution. (Contributed by NM, 5-Aug-1993.) (Proof revised by Jim Kingdon, 20-Jan-2018.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥](𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sbft 1742 | Substitution has no effect on a non-free variable. (Contributed by NM, 30-May-2009.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 3-May-2018.) |
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑)) | ||
Theorem | sbid2h 1743 | An identity law for substitution. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑) | ||
Theorem | sbid2 1744 | An identity law for substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑) | ||
Theorem | sbidm 1745 | An idempotent law for substitution. (Contributed by NM, 30-Jun-1994.) (Proof rewritten by Jim Kingdon, 21-Jan-2018.) |
⊢ ([𝑦 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | sb5rf 1746 | Reversed substitution. (Contributed by NM, 3-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (𝜑 ↔ ∃𝑦(𝑦 = 𝑥 ∧ [𝑦 / 𝑥]𝜑)) | ||
Theorem | sb6rf 1747 | Reversed substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥]𝜑)) | ||
Theorem | sb8h 1748 | Substitution of variable in universal quantifier. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Jim Kingdon, 15-Jan-2018.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb8eh 1749 | Substitution of variable in existential quantifier. (Contributed by NM, 12-Aug-1993.) (Proof rewritten by Jim Kingdon, 15-Jan-2018.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb8 1750 | Substitution of variable in universal quantifier. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Jim Kingdon, 15-Jan-2018.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb8e 1751 | Substitution of variable in existential quantifier. (Contributed by NM, 12-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Jim Kingdon, 15-Jan-2018.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | ax16i 1752* | Inference with ax-16 1709 as its conclusion, that doesn't require ax-10 1410, ax-11 1411, or ax-12 1416 for its proof. The hypotheses may be eliminable without one or more of these axioms in special cases. (Contributed by NM, 20-May-2008.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | ax16ALT 1753* | Version of ax16 1708 that doesn't require ax-10 1410 or ax-12 1416 for its proof. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | spv 1754* | Specialization, using implicit substitition. (Contributed by NM, 30-Aug-1993.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spimev 1755* | Distinct-variable version of spime 1643. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | speiv 1756* | Inference from existential specialization, using implicit substitition. (Contributed by NM, 19-Aug-1993.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ ∃𝑥𝜑 | ||
Theorem | equvin 1757* | A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝑥 = 𝑦 ↔ ∃𝑧(𝑥 = 𝑧 ∧ 𝑧 = 𝑦)) | ||
Theorem | a16g 1758* | A generalization of axiom ax-16 1709. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
Theorem | a16gb 1759* | A generalization of axiom ax-16 1709. (Contributed by NM, 5-Aug-1993.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ ∀𝑧𝜑)) | ||
Theorem | a16nf 1760* | If there is only one element in the universe, then everything satisfies Ⅎ. (Contributed by Mario Carneiro, 7-Oct-2016.) |
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) | ||
Theorem | 2albidv 1761* | Formula-building rule for 2 existential quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 ↔ ∀𝑥∀𝑦𝜒)) | ||
Theorem | 2exbidv 1762* | Formula-building rule for 2 existential quantifiers (deduction rule). (Contributed by NM, 1-May-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒)) | ||
Theorem | 3exbidv 1763* | Formula-building rule for 3 existential quantifiers (deduction rule). (Contributed by NM, 1-May-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧𝜓 ↔ ∃𝑥∃𝑦∃𝑧𝜒)) | ||
Theorem | 4exbidv 1764* | Formula-building rule for 4 existential quantifiers (deduction rule). (Contributed by NM, 3-Aug-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧∃𝑤𝜓 ↔ ∃𝑥∃𝑦∃𝑧∃𝑤𝜒)) | ||
Theorem | 19.9v 1765* | Special case of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-May-1995.) (Revised by NM, 21-May-2007.) |
⊢ (∃𝑥𝜑 ↔ 𝜑) | ||
Theorem | exlimdd 1766 | Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | 19.21v 1767* | Special case of Theorem 19.21 of [Margaris] p. 90. Notational convention: We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as (𝜑 → ∀𝑥𝜑) in 19.21 1489 via the use of distinct variable conditions combined with ax-17 1433. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the distinct variable condition; e.g. euf 1919 derived from df-eu 1917. The "f" stands for "not free in" which is less restrictive than "does not occur in." (Contributed by NM, 5-Aug-1993.) |
⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) | ||
Theorem | alrimiv 1768* | Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥𝜓) | ||
Theorem | alrimivv 1769* | Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) | ||
Theorem | alrimdv 1770* | Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 10-Feb-1997.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) | ||
Theorem | nfdv 1771* | Apply the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝜓) | ||
Theorem | 2ax17 1772* | Quantification of two variables over a formula in which they do not occur. (Contributed by Alan Sare, 12-Apr-2011.) |
⊢ (𝜑 → ∀𝑥∀𝑦𝜑) | ||
Theorem | alimdv 1773* | Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 3-Apr-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) | ||
Theorem | eximdv 1774* | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) | ||
Theorem | 2alimdv 1775* | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-2004.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜒)) | ||
Theorem | 2eximdv 1776* | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 3-Aug-1995.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) | ||
Theorem | 19.23v 1777* | Special case of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jun-1998.) |
⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) | ||
Theorem | 19.23vv 1778* | Theorem 19.23 of [Margaris] p. 90 extended to two variables. (Contributed by NM, 10-Aug-2004.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥∃𝑦𝜑 → 𝜓)) | ||
Theorem | sb56 1779* | Two equivalent ways of expressing the proper substitution of 𝑦 for 𝑥 in 𝜑, when 𝑥 and 𝑦 are distinct. Theorem 6.2 of [Quine] p. 40. The proof does not involve df-sb 1660. (Contributed by NM, 14-Apr-2008.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb6 1780* | Equivalence for substitution. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70. (Contributed by NM, 18-Aug-1993.) (Revised by NM, 14-Apr-2008.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb5 1781* | Equivalence for substitution. Similar to Theorem 6.1 of [Quine] p. 40. (Contributed by NM, 18-Aug-1993.) (Revised by NM, 14-Apr-2008.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sbnv 1782* | Version of sbn 1840 where 𝑥 and 𝑦 are distinct. (Contributed by Jim Kingdon, 18-Dec-2017.) |
⊢ ([𝑦 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑦 / 𝑥]𝜑) | ||
Theorem | sbanv 1783* | Version of sban 1843 where 𝑥 and 𝑦 are distinct. (Contributed by Jim Kingdon, 24-Dec-2017.) |
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sborv 1784* | Version of sbor 1842 where 𝑥 and 𝑦 are distinct. (Contributed by Jim Kingdon, 3-Feb-2018.) |
⊢ ([𝑦 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbi1v 1785* | Forward direction of sbimv 1787. (Contributed by Jim Kingdon, 25-Dec-2017.) |
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbi2v 1786* | Reverse direction of sbimv 1787. (Contributed by Jim Kingdon, 18-Jan-2018.) |
⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 → 𝜓)) | ||
Theorem | sbimv 1787* | Intuitionistic proof of sbim 1841 where 𝑥 and 𝑦 are distinct. (Contributed by Jim Kingdon, 18-Jan-2018.) |
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sblimv 1788* | Version of sblim 1845 where 𝑥 and 𝑦 are distinct. (Contributed by Jim Kingdon, 19-Jan-2018.) |
⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → 𝜓)) | ||
Theorem | pm11.53 1789* | Theorem *11.53 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)) | ||
Theorem | exlimivv 1790* | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 1-Aug-1995.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) | ||
Theorem | exlimdvv 1791* | Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒)) | ||
Theorem | exlimddv 1792* | Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.) |
⊢ (𝜑 → ∃𝑥𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | 19.27v 1793* | Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 3-Jun-2004.) |
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓)) | ||
Theorem | 19.28v 1794* | Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 25-Mar-2004.) |
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓)) | ||
Theorem | 19.36aiv 1795* | Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
⊢ ∃𝑥(𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | 19.41v 1796* | Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) | ||
Theorem | 19.41vv 1797* | Theorem 19.41 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 30-Apr-1995.) |
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓)) | ||
Theorem | 19.41vvv 1798* | Theorem 19.41 of [Margaris] p. 90 with 3 quantifiers. (Contributed by NM, 30-Apr-1995.) |
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦∃𝑧𝜑 ∧ 𝜓)) | ||
Theorem | 19.41vvvv 1799* | Theorem 19.41 of [Margaris] p. 90 with 4 quantifiers. (Contributed by FL, 14-Jul-2007.) |
⊢ (∃𝑤∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (∃𝑤∃𝑥∃𝑦∃𝑧𝜑 ∧ 𝜓)) | ||
Theorem | 19.42v 1800* | Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |