![]() |
Metamath
Proof Explorer Theorem List (p. 21 of 483) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30721) |
![]() (30722-32244) |
![]() (32245-48210) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | equsexvw 2001* | Version of equsexv 2252 with a disjoint variable condition, and of equsex 2412 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2000. (Contributed by BJ, 31-May-2019.) (Proof shortened by Wolf Lammen, 23-Oct-2023.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | cbvaliw 2002* | Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by NM, 19-Apr-2017.) |
⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) & ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | cbvalivw 2003* | Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by NM, 9-Apr-2017.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Axiom | ax-7 2004 |
Axiom of Equality. One of the equality and substitution axioms of
predicate calculus with equality. It states that equality is a
right-Euclidean binary relation (this is similar, but not identical, to
being transitive, which is proved as equtr 2017). This axiom scheme is a
sub-scheme of Axiom Scheme B8 of system S2 of [Tarski], p. 75, whose
general form cannot be represented with our notation. Also appears as
Axiom C7 of [Monk2] p. 105 and Axiom Scheme
C8' in [Megill] p. 448 (p. 16
of the preprint).
The equality symbol was invented in 1557 by Robert Recorde. He chose a pair of parallel lines of the same length because "noe .2. thynges, can be moare equalle". We prove in ax7 2012 that this axiom can be recovered from its weakened version ax7v 2005 where 𝑥 and 𝑦 are assumed to be disjoint variables. In particular, the only theorem referencing ax-7 2004 should be ax7v 2005. See the comment of ax7v 2005 for more details on these matters. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 7-Dec-2020.) Use ax7 2012 instead. (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | ||
Theorem | ax7v 2005* |
Weakened version of ax-7 2004, with a disjoint variable condition on
𝑥,
𝑦. This should be
the only proof referencing ax-7 2004, and it
should be referenced only by its two weakened versions ax7v1 2006 and
ax7v2 2007, from which ax-7 2004
is then rederived as ax7 2012, which shows
that either ax7v 2005 or the conjunction of ax7v1 2006 and ax7v2 2007 is
sufficient.
In ax7v 2005, it is still allowed to substitute the same variable for 𝑥 and 𝑧, or the same variable for 𝑦 and 𝑧. Therefore, ax7v 2005 "bundles" (a term coined by Raph Levien) its "principal instance" (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) with 𝑥, 𝑦, 𝑧 distinct, and its "degenerate instances" (𝑥 = 𝑦 → (𝑥 = 𝑥 → 𝑦 = 𝑥)) and (𝑥 = 𝑦 → (𝑥 = 𝑦 → 𝑦 = 𝑦)) with 𝑥, 𝑦 distinct. These degenerate instances are for instance used in the proofs of equcomiv 2010 and equid 2008 respectively. (Contributed by BJ, 7-Dec-2020.) Use ax7 2012 instead. (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | ||
Theorem | ax7v1 2006* | First of two weakened versions of ax7v 2005, with an extra disjoint variable condition on 𝑥, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | ||
Theorem | ax7v2 2007* | Second of two weakened versions of ax7v 2005, with an extra disjoint variable condition on 𝑦, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | ||
Theorem | equid 2008 | Identity law for equality. Lemma 2 of [KalishMontague] p. 85. See also Lemma 6 of [Tarski] p. 68. (Contributed by NM, 1-Apr-2005.) (Revised by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 22-Aug-2020.) |
⊢ 𝑥 = 𝑥 | ||
Theorem | nfequid 2009 | Bound-variable hypothesis builder for 𝑥 = 𝑥. This theorem tells us that any variable, including 𝑥, is effectively not free in 𝑥 = 𝑥, even though 𝑥 is technically free according to the traditional definition of free variable. (Contributed by NM, 13-Jan-2011.) (Revised by NM, 21-Aug-2017.) |
⊢ Ⅎ𝑦 𝑥 = 𝑥 | ||
Theorem | equcomiv 2010* | Weaker form of equcomi 2013 with a disjoint variable condition on 𝑥, 𝑦. This is an intermediate step and equcomi 2013 is fully recovered later. (Contributed by BJ, 7-Dec-2020.) |
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) | ||
Theorem | ax6evr 2011* | A commuted form of ax6ev 1966. (Contributed by BJ, 7-Dec-2020.) |
⊢ ∃𝑥 𝑦 = 𝑥 | ||
Theorem | ax7 2012 |
Proof of ax-7 2004 from ax7v1 2006 and ax7v2 2007 (and earlier axioms), proving
sufficiency of the conjunction of the latter two weakened versions of
ax7v 2005, which is itself a weakened version of ax-7 2004.
Note that the weakened version of ax-7 2004 obtained by adding a disjoint variable condition on 𝑥, 𝑧 (resp. on 𝑦, 𝑧) does not permit, together with the other axioms, to prove reflexivity (resp. symmetry). (Contributed by BJ, 7-Dec-2020.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | ||
Theorem | equcomi 2013 | Commutative law for equality. Equality is a symmetric relation. Lemma 3 of [KalishMontague] p. 85. See also Lemma 7 of [Tarski] p. 69. (Contributed by NM, 10-Jan-1993.) (Revised by NM, 9-Apr-2017.) |
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) | ||
Theorem | equcom 2014 | Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.) |
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) | ||
Theorem | equcomd 2015 | Deduction form of equcom 2014, symmetry of equality. For the versions for classes, see eqcom 2734 and eqcomd 2733. (Contributed by BJ, 6-Oct-2019.) |
⊢ (𝜑 → 𝑥 = 𝑦) ⇒ ⊢ (𝜑 → 𝑦 = 𝑥) | ||
Theorem | equcoms 2016 | An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 10-Jan-1993.) |
⊢ (𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (𝑦 = 𝑥 → 𝜑) | ||
Theorem | equtr 2017 | A transitive law for equality. (Contributed by NM, 23-Aug-1993.) |
⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧)) | ||
Theorem | equtrr 2018 | A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.) |
⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦)) | ||
Theorem | equeuclr 2019 | Commuted version of equeucl 2020 (equality is left-Euclidean). (Contributed by BJ, 12-Apr-2021.) |
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑦 = 𝑥)) | ||
Theorem | equeucl 2020 | Equality is a left-Euclidean binary relation. (Right-Euclideanness is stated in ax-7 2004.) Curried (exported) form of equtr2 2023. (Contributed by BJ, 11-Apr-2021.) |
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑥 = 𝑦)) | ||
Theorem | equequ1 2021 | An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧)) | ||
Theorem | equequ2 2022 | An equivalence law for equality. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.) (Proof shortened by BJ, 12-Apr-2021.) |
⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) | ||
Theorem | equtr2 2023 | Equality is a left-Euclidean binary relation. Uncurried (imported) form of equeucl 2020. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by BJ, 11-Apr-2021.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑦) | ||
Theorem | stdpc6 2024 | One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 2235.) Axiom 6 of [Mendelson] p. 95. Mendelson doesn't say why he prepended the redundant quantifier, but it was probably to be compatible with free logic (which is valid in the empty domain). (Contributed by NM, 16-Feb-2005.) |
⊢ ∀𝑥 𝑥 = 𝑥 | ||
Theorem | equvinv 2025* | A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. (Contributed by NM, 9-Jan-1993.) Remove dependencies on ax-10 2130, ax-13 2366. (Revised by Wolf Lammen, 10-Jun-2019.) Move the quantified variable (𝑧) to the left of the equality signs. (Revised by Wolf Lammen, 11-Apr-2021.) (Proof shortened by Wolf Lammen, 12-Jul-2022.) |
⊢ (𝑥 = 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 = 𝑦)) | ||
Theorem | equvinva 2026* | A modified version of the forward implication of equvinv 2025 adapted to common usage. (Contributed by Wolf Lammen, 8-Sep-2018.) |
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑥 = 𝑧 ∧ 𝑦 = 𝑧)) | ||
Theorem | equvelv 2027* | A biconditional form of equvel 2450 with disjoint variable conditions and proved from Tarski's FOL axiom schemes. (Contributed by Andrew Salmon, 2-Jun-2011.) Reduce axiom usage. (Revised by Wolf Lammen, 10-Apr-2021.) (Proof shortened by Wolf Lammen, 12-Jul-2022.) |
⊢ (∀𝑧(𝑧 = 𝑥 → 𝑧 = 𝑦) ↔ 𝑥 = 𝑦) | ||
Theorem | ax13b 2028 | An equivalence between two ways of expressing ax-13 2366. See the comment for ax-13 2366. (Contributed by NM, 2-May-2017.) (Proof shortened by Wolf Lammen, 26-Feb-2018.) (Revised by BJ, 15-Sep-2020.) |
⊢ ((¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝜑)) ↔ (¬ 𝑥 = 𝑦 → (¬ 𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝜑)))) | ||
Theorem | spfw 2029* | Weak version of sp 2169. Uses only Tarski's FOL axiom schemes. Lemma 9 of [KalishMontague] p. 87. This may be the best we can do with minimal distinct variable conditions. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 10-Oct-2021.) |
⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) & ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) & ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | spw 2030* | Weak version of the specialization scheme sp 2169. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2169 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2169 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2124 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2169 are spfw 2029 (minimal distinct variable requirements), spnfw 1976 (when 𝑥 is not free in ¬ 𝜑), spvw 1977 (when 𝑥 does not appear in 𝜑), sptruw 1801 (when 𝜑 is true), spfalw 1994 (when 𝜑 is false), and spvv 1993 (where 𝜑 is changed into 𝜓). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | cbvalw 2031* | Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) |
⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) & ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) & ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓) & ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvalvw 2032* | Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2394 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvexvw 2033* | Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2395 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 19-Apr-2017.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbvaldvaw 2034* | Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Version of cbvaldva 2403 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2366. (Revised by Gino Giotto, 10-Jan-2024.) Reduce axiom usage, along an idea of Gino Giotto. (Revised by Wolf Lammen, 10-Feb-2024.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvexdvaw 2035* | Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva 2404 with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017.) Avoid ax-13 2366. (Revised by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Wolf Lammen, 10-Feb-2024.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbval2vw 2036* | Rule used to change bound variables, using implicit substitution. Version of cbval2vv 2407 with more disjoint variable conditions, which requires fewer axioms . (Contributed by NM, 4-Feb-2005.) Avoid ax-13 2366. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbvex2vw 2037* | Rule used to change bound variables, using implicit substitution. Version of cbvex2vv 2408 with more disjoint variable conditions, which requires fewer axioms . (Contributed by NM, 26-Jul-1995.) Avoid ax-13 2366. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | cbvex4vw 2038* | Rule used to change bound variables, using implicit substitution. Version of cbvex4v 2409 with more disjoint variable conditions, which requires fewer axioms. (Contributed by NM, 26-Jul-1995.) Avoid ax-13 2366. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒) | ||
Theorem | alcomiw 2039* | Weak version of ax-11 2147. See alcomw 2040 for the biconditional form. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Dec-2023.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | alcomw 2040* | Weak version of alcom 2149 and biconditional form of alcomiw 2039. Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 28-Dec-2024.) |
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑦∀𝑥𝜑) | ||
Theorem | hbn1fw 2041* | Weak version of ax-10 2130 from which we can prove any ax-10 2130 instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.) |
⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) & ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) & ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓) & ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) & ⊢ (¬ ∀𝑦𝜓 → ∀𝑥 ¬ ∀𝑦𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑) | ||
Theorem | hbn1w 2042* | Weak version of hbn1 2131. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑) | ||
Theorem | hba1w 2043* | Weak version of hba1 2282. See comments for ax10w 2118. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 10-Oct-2021.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) | ||
Theorem | hbe1w 2044* | Weak version of hbe1 2132. See comments for ax10w 2118. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | ||
Theorem | hbalw 2045* | Weak version of hbal 2160. Uses only Tarski's FOL axiom schemes. Unlike hbal 2160, this theorem requires that 𝑥 and 𝑦 be distinct, i.e., not be bundled. (Contributed by NM, 19-Apr-2017.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) | ||
Theorem | 19.8aw 2046* | If a formula is true, then it is true for at least one instance. This is to 19.8a 2167 what spw 2030 is to sp 2169. (Contributed by SN, 26-Sep-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝜑 → ∃𝑥𝜑) | ||
Theorem | exexw 2047* | Existential quantification over a given variable is idempotent. Weak version of bj-exexbiex 36167, requiring fewer axioms. (Contributed by Gino Giotto, 4-Nov-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑥∃𝑥𝜑) | ||
Theorem | spaev 2048* |
A special instance of sp 2169 applied to an equality with a disjoint
variable condition. Unlike the more general sp 2169, we
can prove this
without ax-12 2164. Instance of aeveq 2052.
The antecedent ∀𝑥𝑥 = 𝑦 with distinct 𝑥 and 𝑦 is a characteristic of a degenerate universe, in which just one object exists. Actually more than one object may still exist, but if so, we give up on equality as a discriminating term. Separating this degenerate case from a richer universe, where inequality is possible, is a common proof idea. The name of this theorem follows a convention, where the condition ∀𝑥𝑥 = 𝑦 is denoted by 'aev', a shorthand for 'all equal, with a distinct variable condition'. (Contributed by Wolf Lammen, 14-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦) | ||
Theorem | cbvaev 2049* | Change bound variable in an equality with a disjoint variable condition. Instance of aev 2053. (Contributed by NM, 22-Jul-2015.) (Revised by BJ, 18-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑦) | ||
Theorem | aevlem0 2050* | Lemma for aevlem 2051. Instance of aev 2053. (Contributed by NM, 8-Jul-2016.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-12 2164. (Revised by Wolf Lammen, 14-Mar-2021.) (Revised by BJ, 29-Mar-2021.) (Proof shortened by Wolf Lammen, 30-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑥) | ||
Theorem | aevlem 2051* | Lemma for aev 2053 and axc16g 2244. Change free and bound variables. Instance of aev 2053. (Contributed by NM, 22-Jul-2015.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-13 2366, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 29-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑡) | ||
Theorem | aeveq 2052* | The antecedent ∀𝑥𝑥 = 𝑦 with a disjoint variable condition (typical of a one-object universe) forces equality of everything. (Contributed by Wolf Lammen, 19-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝑧 = 𝑡) | ||
Theorem | aev 2053* | A "distinctor elimination" lemma with no disjoint variable conditions on variables in the consequent. (Contributed by NM, 8-Nov-2006.) Remove dependency on ax-11 2147. (Revised by Wolf Lammen, 7-Sep-2018.) Remove dependency on ax-13 2366, inspired by an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) Remove dependency on ax-12 2164. (Revised by Wolf Lammen, 19-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑡 = 𝑢) | ||
Theorem | aev2 2054* |
A version of aev 2053 with two universal quantifiers in the
consequent.
One can prove similar statements with arbitrary numbers of universal
quantifiers in the consequent (the series begins with aeveq 2052, aev 2053,
aev2 2054).
Using aev 2053 and alrimiv 1923, one can actually prove (with no more axioms) any scheme of the form (∀𝑥𝑥 = 𝑦 → PHI) , DV (𝑥, 𝑦) where PHI involves only setvar variables and the connectors →, ↔, ∧, ∨, ⊤, =, ∀, ∃, ∃*, ∃!, Ⅎ. An example is given by aevdemo 30263. This list cannot be extended to ¬ or ⊥ since the scheme ∀𝑥𝑥 = 𝑦 is consistent with ax-mp 5, ax-gen 1790, ax-1 6-- ax-13 2366 (as the one-element universe shows), so for instance (∀𝑥𝑥 = 𝑦 → ⊥), DV (𝑥, 𝑦) is not provable from these axioms alone (indeed, dtru 5432 uses non-logical axioms as well). (Contributed by BJ, 23-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑡 𝑢 = 𝑣) | ||
Theorem | hbaev 2055* | All variables are effectively bound in an identical variable specifier. Version of hbae 2425 with a disjoint variable condition, requiring fewer axioms. Instance of aev2 2054. (Contributed by NM, 13-May-1993.) (Revised by Wolf Lammen, 22-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦) | ||
Theorem | naev 2056* | If some set variables can assume different values, then any two distinct set variables cannot always be the same. (Contributed by Wolf Lammen, 10-Aug-2019.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑢 𝑢 = 𝑣) | ||
Theorem | naev2 2057* | Generalization of hbnaev 2058. (Contributed by Wolf Lammen, 9-Apr-2021.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑡 𝑡 = 𝑢) | ||
Theorem | hbnaev 2058* | Any variable is free in ¬ ∀𝑥𝑥 = 𝑦, if 𝑥 and 𝑦 are distinct. This condition is dropped in hbnae 2426, at the expense of more axiom dependencies. Instance of naev2 2057. (Contributed by NM, 13-May-1993.) (Revised by Wolf Lammen, 9-Apr-2021.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | sbjust 2059* | Justification theorem for df-sb 2061 proved from Tarski's FOL axiom schemes. (Contributed by BJ, 22-Jan-2023.) |
⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) | ||
Syntax | wsb 2060 | Extend wff definition to include proper substitution. Read: "the wff that results when 𝑦 is properly substituted for 𝑥 in wff 𝜑". (Contributed by NM, 24-Jan-2006.) |
wff [𝑦 / 𝑥]𝜑 | ||
Definition | df-sb 2061* |
Define proper substitution. For our notation, we use [𝑡 / 𝑥]𝜑
to mean "the wff that results from the proper substitution of 𝑡 for
𝑥 in the wff 𝜑". That is, 𝑡
properly replaces 𝑥.
For example, [𝑡 / 𝑥]𝑧 ∈ 𝑥 is the same as 𝑧 ∈ 𝑡 (when 𝑥
and 𝑧 are distinct), as shown in elsb2 2116.
Our notation was introduced in Haskell B. Curry's Foundations of Mathematical Logic (1977), p. 316 and is frequently used in textbooks of lambda calculus and combinatory logic. This notation improves the common but ambiguous notation, "𝜑(𝑡) is the wff that results when 𝑡 is properly substituted for 𝑥 in 𝜑(𝑥)". For example, if the original 𝜑(𝑥) is 𝑥 = 𝑡, then 𝜑(𝑡) is 𝑡 = 𝑡, from which we obtain that 𝜑(𝑥) is 𝑥 = 𝑥. So what exactly does 𝜑(𝑥) mean? Curry's notation solves this problem. A very similar notation, namely (𝑦 ∣ 𝑥)𝜑, was introduced in Bourbaki's Set Theory (Chapter 1, Description of Formal Mathematic, 1953). In most books, proper substitution has a somewhat complicated recursive definition with multiple cases based on the occurrences of free and bound variables in the wff. Instead, we use a single formula that is exactly equivalent and gives us a direct definition. We later prove that our definition has the properties we expect of proper substitution (see Theorems sbequ 2079, sbcom2 2154 and sbid2v 2503). Note that our definition is valid even when 𝑥 and 𝑡 are replaced with the same variable, as sbid 2240 shows. We achieve this by applying twice Tarski's definition sb6 2081 which is valid for disjoint variables, and introducing a dummy variable 𝑦 which isolates 𝑥 from 𝑡, as in dfsb7 2268 with respect to sb5 2260. We can also achieve this by having 𝑥 free in the first conjunct and bound in the second, as the alternate definition dfsb1 2475 shows. Another version that mixes free and bound variables is dfsb3 2488. When 𝑥 and 𝑡 are distinct, we can express proper substitution with the simpler expressions of sb5 2260 and sb6 2081. Note that the occurrences of a given variable in the definiens are either all bound (𝑥, 𝑦) or all free (𝑡). Also note that the definiens uses only primitive symbols. This double level definition will make several proofs using it appear as doubled. Alternately, one could often first prove as a lemma the same theorem with a disjoint variable condition on the substitute and the substituted variables, and then prove the original theorem by applying this lemma twice in a row. (Contributed by NM, 10-May-1993.) Revised from the original definition dfsb1 2475. (Revised by BJ, 22-Dec-2020.) |
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | sbt 2062 | A substitution into a theorem yields a theorem. See sbtALT 2065 for a shorter proof requiring more axioms. See chvar 2389 and chvarv 2390 for versions using implicit substitution. (Contributed by NM, 21-Jan-2004.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Jul-2018.) Revise df-sb 2061. (Revised by Steven Nguyen, 6-Jul-2023.) |
⊢ 𝜑 ⇒ ⊢ [𝑡 / 𝑥]𝜑 | ||
Theorem | sbtru 2063 | The result of substituting in the truth constant "true" is true. (Contributed by BJ, 2-Sep-2023.) |
⊢ [𝑦 / 𝑥]⊤ | ||
Theorem | stdpc4 2064 | The specialization axiom of standard predicate calculus. It states that if a statement 𝜑 holds for all 𝑥, then it also holds for the specific case of 𝑡 (properly) substituted for 𝑥. Translated to traditional notation, it can be read: "∀𝑥𝜑(𝑥) → 𝜑(𝑡), provided that 𝑡 is free for 𝑥 in 𝜑(𝑥)". Axiom 4 of [Mendelson] p. 69. See also spsbc 3787 and rspsbc 3869. (Contributed by NM, 14-May-1993.) Revise df-sb 2061. (Revised by BJ, 22-Dec-2020.) |
⊢ (∀𝑥𝜑 → [𝑡 / 𝑥]𝜑) | ||
Theorem | sbtALT 2065 | Alternate proof of sbt 2062, shorter but using ax-4 1804 and ax-5 1906. (Contributed by NM, 21-Jan-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 ⇒ ⊢ [𝑦 / 𝑥]𝜑 | ||
Theorem | 2stdpc4 2066 | A double specialization using explicit substitution. This is Theorem PM*11.1 in [WhiteheadRussell] p. 159. See stdpc4 2064 for the analogous single specialization. See 2sp 2172 for another double specialization. (Contributed by Andrew Salmon, 24-May-2011.) (Revised by BJ, 21-Oct-2018.) |
⊢ (∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) | ||
Theorem | sbi1 2067 | Distribute substitution over implication. (Contributed by NM, 14-May-1993.) Remove dependencies on axioms. (Revised by Steven Nguyen, 24-Jul-2023.) |
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | spsbim 2068 | Distribute substitution over implication. Closed form of sbimi 2070. Specialization of implication. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) Revise df-sb 2061. (Revised by BJ, 22-Dec-2020.) (Proof shortened by Steven Nguyen, 24-Jul-2023.) |
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)) | ||
Theorem | spsbbi 2069 | Biconditional property for substitution. Closed form of sbbii 2072. Specialization of biconditional. (Contributed by NM, 2-Jun-1993.) Revise df-sb 2061. (Revised by BJ, 22-Dec-2020.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓)) | ||
Theorem | sbimi 2070 | Distribute substitution over implication. (Contributed by NM, 25-Jun-1998.) Revise df-sb 2061. (Revised by BJ, 22-Dec-2020.) (Proof shortened by Steven Nguyen, 24-Jul-2023.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓) | ||
Theorem | sb2imi 2071 | Distribute substitution over implication. Compare al2imi 1810. (Contributed by Steven Nguyen, 13-Aug-2023.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ ([𝑡 / 𝑥]𝜑 → ([𝑡 / 𝑥]𝜓 → [𝑡 / 𝑥]𝜒)) | ||
Theorem | sbbii 2072 | Infer substitution into both sides of a logical equivalence. (Contributed by NM, 14-May-1993.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑥]𝜓) | ||
Theorem | 2sbbii 2073 | Infer double substitution into both sides of a logical equivalence. (Contributed by AV, 30-Jul-2023.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑡 / 𝑥][𝑢 / 𝑦]𝜑 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜓) | ||
Theorem | sbimdv 2074* | Deduction substituting both sides of an implication, with 𝜑 and 𝑥 disjoint. See also sbimd 2230. (Contributed by Wolf Lammen, 6-May-2023.) Revise df-sb 2061. (Revised by Steven Nguyen, 6-Jul-2023.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ([𝑡 / 𝑥]𝜓 → [𝑡 / 𝑥]𝜒)) | ||
Theorem | sbbidv 2075* | Deduction substituting both sides of a biconditional, with 𝜑 and 𝑥 disjoint. See also sbbid 2231. (Contributed by Wolf Lammen, 6-May-2023.) (Proof shortened by Steven Nguyen, 6-Jul-2023.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑡 / 𝑥]𝜓 ↔ [𝑡 / 𝑥]𝜒)) | ||
Theorem | sban 2076 | Conjunction inside and outside of a substitution are equivalent. Compare 19.26 1866. (Contributed by NM, 14-May-1993.) (Proof shortened by Steven Nguyen, 13-Aug-2023.) |
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sb3an 2077 | Threefold conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-Dec-2006.) |
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)) | ||
Theorem | spsbe 2078 | Existential generalization: if a proposition is true for a specific instance, then there exists an instance where it is true. (Contributed by NM, 29-Jun-1993.) (Proof shortened by Wolf Lammen, 3-May-2018.) Revise df-sb 2061. (Revised by BJ, 22-Dec-2020.) (Proof shortened by Steven Nguyen, 11-Jul-2023.) |
⊢ ([𝑡 / 𝑥]𝜑 → ∃𝑥𝜑) | ||
Theorem | sbequ 2079 | Equality property for substitution, from Tarski's system. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 14-May-1993.) Revise df-sb 2061. (Revised by BJ, 30-Dec-2020.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) | ||
Theorem | sbequi 2080 | An equality theorem for substitution. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 15-Sep-2018.) (Proof shortened by Steven Nguyen, 7-Jul-2023.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) | ||
Theorem | sb6 2081* | Alternate definition of substitution when variables are disjoint. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70. The implication "to the left" also holds without a disjoint variable condition (sb2 2473). Theorem sb6f 2491 replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b 2469 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2061. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2147. (Revised by Steven Nguyen, 7-Jul-2023.) (Proof shortened by Wolf Lammen, 16-Jul-2023.) |
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) | ||
Theorem | 2sb6 2082* | Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.) |
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) | ||
Theorem | sb1v 2083* | One direction of sb5 2260, provable from fewer axioms. Version of sb1 2472 with a disjoint variable condition using fewer axioms. (Contributed by NM, 13-May-1993.) (Revised by Wolf Lammen, 20-Jan-2024.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sbv 2084* | Substitution for a variable not occurring in a proposition. See sbf 2255 for a version without disjoint variable condition on 𝑥, 𝜑. If one adds a disjoint variable condition on 𝑥, 𝑡, then sbv 2084 can be proved directly by chaining equsv 1999 with sb6 2081. (Contributed by BJ, 22-Dec-2020.) |
⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜑) | ||
Theorem | sbcom4 2085* | Commutativity law for substitution. This theorem was incorrectly used as our previous version of pm11.07 2086 but may still be useful. (Contributed by Andrew Salmon, 17-Jun-2011.) (Proof shortened by Jim Kingdon, 22-Jan-2018.) |
⊢ ([𝑤 / 𝑥][𝑦 / 𝑧]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑) | ||
Theorem | pm11.07 2086 | Axiom *11.07 in [WhiteheadRussell] p. 159. The original reads: *11.07 "Whatever possible argument 𝑥 may be, 𝜑(𝑥, 𝑦) is true whatever possible argument 𝑦 may be" implies the corresponding statement with 𝑥 and 𝑦 interchanged except in "𝜑(𝑥, 𝑦)". Under our formalism this appears to correspond to idi 1 and not to sbcom4 2085 as earlier thought. See https://groups.google.com/g/metamath/c/iS0fOvSemC8/m/M1zTH8wxCAAJ 2085. (Contributed by BJ, 16-Sep-2018.) (New usage is discouraged.) |
⊢ 𝜑 ⇒ ⊢ 𝜑 | ||
Theorem | sbrimvw 2087* | Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim 2293 based on fewer axioms, but with more disjoint variable conditions. Based on an idea of Gino Giotto. (Contributed by Wolf Lammen, 29-Jan-2024.) |
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbievw 2088* | Conversion of implicit substitution to explicit substitution. Version of sbie 2496 and sbiev 2303 with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by BJ, 18-Jul-2023.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) | ||
Theorem | sbiedvw 2089* | Conversion of implicit substitution to explicit substitution (deduction version of sbievw 2088). Version of sbied 2497 and sbiedv 2498 with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Gino Giotto, 29-Jan-2024.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | 2sbievw 2090* | Conversion of double implicit substitution to explicit substitution. Version of 2sbiev 2499 with more disjoint variable conditions, requiring fewer axioms. (Contributed by AV, 29-Jul-2023.) Avoid ax-13 2366. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑡 / 𝑥][𝑢 / 𝑦]𝜑 ↔ 𝜓) | ||
Theorem | sbcom3vv 2091* | Substituting 𝑦 for 𝑥 and then 𝑧 for 𝑦 is equivalent to substituting 𝑧 for both 𝑥 and 𝑦. Version of sbcom3 2500 with a disjoint variable condition using fewer axioms. (Contributed by NM, 27-May-1997.) (Revised by Giovanni Mascellani, 8-Apr-2018.) (Revised by BJ, 30-Dec-2020.) (Proof shortened by Wolf Lammen, 19-Jan-2023.) |
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑧 / 𝑥]𝜑) | ||
Theorem | sbievw2 2092* | sbievw 2088 applied twice, avoiding a DV condition on 𝑥, 𝑦. Based on proofs by Wolf Lammen. (Contributed by Steven Nguyen, 29-Jul-2023.) |
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜒)) & ⊢ (𝑤 = 𝑦 → (𝜒 ↔ 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) | ||
Theorem | sbco2vv 2093* | A composition law for substitution. Version of sbco2 2505 with disjoint variable conditions and fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by BJ, 22-Dec-2020.) (Proof shortened by Wolf Lammen, 29-Apr-2023.) |
⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | equsb3 2094* | Substitution in an equality. (Contributed by Raph Levien and FL, 4-Dec-2005.) Reduce axiom usage. (Revised by Wolf Lammen, 23-Jul-2023.) |
⊢ ([𝑦 / 𝑥]𝑥 = 𝑧 ↔ 𝑦 = 𝑧) | ||
Theorem | equsb3r 2095* | Substitution applied to the atomic wff with equality. Variant of equsb3 2094. (Contributed by AV, 29-Jul-2023.) (Proof shortened by Wolf Lammen, 2-Sep-2023.) |
⊢ ([𝑦 / 𝑥]𝑧 = 𝑥 ↔ 𝑧 = 𝑦) | ||
Theorem | equsb1v 2096* | Substitution applied to an atomic wff. Version of equsb1 2485 with a disjoint variable condition, which neither requires ax-12 2164 nor ax-13 2366. (Contributed by NM, 10-May-1993.) (Revised by BJ, 11-Sep-2019.) Remove dependencies on axioms. (Revised by Wolf Lammen, 30-May-2023.) (Proof shortened by Steven Nguyen, 19-Jun-2023.) Revise df-sb 2061. (Revised by Steven Nguyen, 11-Jul-2023.) (Proof shortened by Steven Nguyen, 22-Jul-2023.) |
⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | ||
Theorem | nsb 2097 | Any substitution in an always false formula is false. (Contributed by Steven Nguyen, 3-May-2023.) |
⊢ (∀𝑥 ¬ 𝜑 → ¬ [𝑡 / 𝑥]𝜑) | ||
Theorem | sbn1 2098 | One direction of sbn 2269, using fewer axioms. Compare 19.2 1973. (Contributed by Steven Nguyen, 18-Aug-2023.) |
⊢ ([𝑡 / 𝑥] ¬ 𝜑 → ¬ [𝑡 / 𝑥]𝜑) | ||
Syntax | wcel 2099 |
Extend wff definition to include the membership connective between
classes.
For a general discussion of the theory of classes, see mmset.html#class. The purpose of introducing wff 𝐴 ∈ 𝐵 here is to allow to prove the wel 2100 of predicate calculus in terms of the wcel 2099 of set theory, so that we do not overload the ∈ connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers. The class variables 𝐴 and 𝐵 are introduced temporarily for the purpose of this definition but otherwise not used in predicate calculus. See df-clab 2705 for more information on the set theory usage of wcel 2099. |
wff 𝐴 ∈ 𝐵 | ||
Theorem | wel 2100 |
Extend wff definition to include atomic formulas with the membership
predicate. This is read either "𝑥 is an element of 𝑦",
or "𝑥 is a member of 𝑦", or "𝑥 belongs
to 𝑦",
or "𝑦 contains 𝑥". Note: The
phrase "𝑦 includes
𝑥 " means "𝑥 is a
subset of 𝑦"; to use it also for
𝑥
∈ 𝑦, as some
authors occasionally do, is poor form and causes
confusion, according to George Boolos (1992 lecture at MIT).
This syntactic construction introduces a binary non-logical predicate symbol ∈ (stylized lowercase epsilon) into our predicate calculus. We will eventually use it for the membership predicate of set theory, but that is irrelevant at this point: the predicate calculus axioms for ∈ apply to any arbitrary binary predicate symbol. "Non-logical" means that the predicate is presumed to have additional properties beyond the realm of predicate calculus, although these additional properties are not specified by predicate calculus itself but rather by the axioms of a theory (in our case set theory) added to predicate calculus. "Binary" means that the predicate has two arguments. Instead of introducing wel 2100 as an axiomatic statement, as was done in an older version of this database, we introduce it by "proving" a special case of set theory's more general wcel 2099. This lets us avoid overloading the ∈ connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 2100 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 2099. Note: To see the proof steps of this syntax proof, type "MM> SHOW PROOF wel / ALL" in the Metamath program. (Contributed by NM, 24-Jan-2006.) |
wff 𝑥 ∈ 𝑦 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |