P. 19 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 1801-1900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sbequ8 1801	Elimination of equality from antecedent after substitution. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Jul-2018.)
|- ( [ y / x ] ph <-> [ y / x ] ( x = y -> ph ) )
Theorem	sbimi 1802	Infer substitution into antecedent and consequent of an implication. (Contributed by NM, 25-Jun-1998.)
|- ( ph -> ps )   =>    |- ( [ y / x ] ph -> [ y / x ] ps )
Theorem	sbbii 1803	Infer substitution into both sides of a logical equivalence. (Contributed by NM, 14-May-1993.)
|- ( ph <-> ps )   =>    |- ( [ y / x ] ph <-> [ y / x ] ps )
1.4.7  Axiom scheme ax-6 (Existence)
Axiom	ax-6 1804	Axiom of Existence. One of the equality and substitution axioms of predicate calculus with equality. This axiom tells us is that at least one thing exists. In this form (not requiring that x and y be distinct) it was used in an axiom system of Tarski (see Axiom B7' in footnote 1 of [KalishMontague] p. 81.) It is equivalent to axiom scheme C10' in [Megill] p. 448 (p. 16 of the preprint); the equivalence is established by axc10 2095 and ax6fromc10 32462. A more convenient form of this axiom is ax6e 2093, which has additional remarks. Raph Levien proved the independence of this axiom from the other logical axioms on 12-Apr-2005. See item 16 at http://us.metamath.org/award2003.html. ax-6 1804 can be proved from the weaker version ax6v 1805 requiring that the variables be distinct; see theorem ax6 2094. ax-6 1804 can also be proved from the Axiom of Separation (in the form that we use that axiom, where free variables are not universally quantified). See theorem ax6vsep 4528. Except by ax6v 1805, this axiom should not be referenced directly. Instead, use theorem ax6 2094. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.)
|- -. A. x -. x = y
Theorem	ax6v 1805*	Axiom B7 of [Tarski] p. 75, which requires that x and y be distinct. This trivial proof is intended merely to weaken axiom ax-6 1804 by adding a distinct variable restriction. From here on, ax-6 1804 should not be referenced directly by any other proof, so that theorem ax6 2094 will show that we can recover ax-6 1804 from this weaker version if it were an axiom (as it is in the case of Tarski). Note: Introducing x , y as a distinct variable group "out of the blue" with no apparent justification has puzzled some people, but it is perfectly sound. All we are doing is adding an additional redundant requirement, no different from adding a redundant logical hypothesis, that results in a weakening of the theorem. This means that any future theorem that references ax6v 1805 must have a $d specified for the two variables that get substituted for x and y. The $d does not propagate "backwards" i.e. it does not impose a requirement on ax-6 1804. When possible, use of this theorem rather than ax6 2094 is preferred since its derivation is much shorter and requires fewer axioms. (Contributed by NM, 7-Aug-2015.)
|- -. A. x -. x = y
Theorem	ax6ev 1806*	At least one individual exists. Weaker version of ax6e 2093. When possible, use of this theorem rather than ax6e 2093 is preferred since its derivation is much shorter and requires fewer axioms. (Contributed by NM, 3-Aug-2017.)
|- E. x x = y
Theorem	exiftru 1807	Rule of existential generalization, similar to universal generalization ax-gen 1668, but valid only if an individual exists. Its proof requires ax-6 1804 but the equality predicate does not occur in its statement. Some fundamental theorems of predicate logic can be proven from ax-gen 1668, ax-4 1681 and this theorem alone, not requiring ax-7 1850 or excessive distinct variable conditions. (Contributed by Wolf Lammen, 12-Nov-2017.) (Proof shortened by Wolf Lammen, 9-Dec-2017.)
|- ph   =>    |- E. x ph
Theorem	19.2 1808	Theorem 19.2 of [Margaris] p. 89. This corresponds to the axiom (D) of modal logic. Note: This proof is very different from Margaris' because we only have Tarski's FOL axiom schemes available at this point. See the later 19.2g 1945 for a more conventional proof of a more general result, which uses additional axioms. (Contributed by NM, 2-Aug-2017.) Remove dependency on ax-7 1850. (Revised by Wolf Lammen, 4-Dec-2017.)
|- ( A. x ph -> E. x ph )
Theorem	19.8w 1809	Weak version of 19.8a 1934. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 4-Dec-2017.)
|- ( ph -> A. x ph )   =>    |- ( ph -> E. x ph )
Theorem	19.8v 1810*	Version of 19.8a 1934 with a dv condition, requiring fewer axioms. (Contributed by BJ, 12-Mar-2020.)
|- ( ph -> E. x ph )
Theorem	19.9v 1811*	Version of 19.9 1969 with a dv condition, requiring fewer axioms. Any formula can be existentially quantified using a variable which it does not contain. See also 19.3v 1812. (Contributed by NM, 28-May-1995.) Remove dependency on ax-7 1850. (Revised by Wolf Lammen, 4-Dec-2017.)
|- ( E. x ph <-> ph )
Theorem	19.3v 1812*	Version of 19.3 1965 with a dv condition, requiring fewer axioms. Any formula can be universally quantified using a variable which it does not contain. See also 19.9v 1811. (Contributed by Anthony Hart, 13-Sep-2011.) Remove dependency on ax-7 1850. (Revised by Wolf Lammen, 4-Dec-2017.)
|- ( A. x ph <-> ph )
Theorem	spvw 1813*	Version of sp 1936 when x does not occur in ph. Converse of ax-5 1757. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.) (Proof shortened by Wolf Lammen, 4-Dec-2017.)
|- ( A. x ph -> ph )
Theorem	19.39 1814	Theorem 19.39 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- ( ( E. x ph -> E. x ps ) -> E. x ( ph -> ps ) )
Theorem	19.24 1815	Theorem 19.24 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- ( ( A. x ph -> A. x ps ) -> E. x ( ph -> ps ) )
Theorem	19.34 1816	Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
|- ( ( A. x ph \/ E. x ps ) -> E. x ( ph \/ ps ) )
Theorem	19.23v 1817*	Version of 19.23 1992 with a dv condition instead of a non-freeness hypothesis. (Contributed by NM, 28-Jun-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020.)
|- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )
Theorem	19.23vv 1818*	Theorem 19.23v 1817 extended to two variables. (Contributed by NM, 10-Aug-2004.)
|- ( A. x A. y ( ph -> ps ) <-> ( E. x E. y ph -> ps ) )
Theorem	19.36v 1819*	Version of 19.36 2043 with a dv condition instead of a non-freeness hypothesis. (Contributed by NM, 18-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 17-Jan-2020.)
|- ( E. x ( ph -> ps ) <-> ( A. x ph -> ps ) )
Theorem	19.36iv 1820*	Inference associated with 19.36v 1819. Version of 19.36i 2044 with a dv condition. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 17-Jan-2020.)
|- E. x ( ph -> ps )   =>    |- ( A. x ph -> ps )
Theorem	pm11.53v 1821*	Version of pm11.53 2072 with a dv condition, requiring fewer axioms. (Contributed by BJ, 7-Mar-2020.)
|- ( A. x A. y ( ph -> ps ) <-> ( E. x ph -> A. y ps ) )
Theorem	19.12vvv 1822*	Version of 19.12vv 2075 with a dv condition, requiring fewer axioms. See also 19.12 2032. (Contributed by BJ, 18-Mar-2020.)
|- ( E. x A. y ( ph -> ps ) <-> A. y E. x ( ph -> ps ) )
Theorem	19.27v 1823*	Version of 19.27 2005 with a dv condition, requiring fewer axioms. (Contributed by NM, 3-Jun-2004.)
|- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ ps ) )
Theorem	19.28v 1824*	Version of 19.28 2006 with a dv condition, requiring fewer axioms. (Contributed by NM, 25-Mar-2004.)
|- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) )
Theorem	19.37v 1825*	Version of 19.37 2045 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
|- ( E. x ( ph -> ps ) <-> ( ph -> E. x ps ) )
Theorem	19.37iv 1826*	Inference associated with 19.37v 1825. (Contributed by NM, 5-Aug-1993.)
|- E. x ( ph -> ps )   =>    |- ( ph -> E. x ps )
Theorem	19.44v 1827*	Version of 19.44 2048 with a dv condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
|- ( E. x ( ph \/ ps ) <-> ( E. x ph \/ ps ) )
Theorem	19.45v 1828*	Version of 19.45 2049 with a dv condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
|- ( E. x ( ph \/ ps ) <-> ( ph \/ E. x ps ) )
Theorem	19.41v 1829*	Version of 19.41 2050 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
|- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) )
Theorem	19.41vv 1830*	Version of 19.41 2050 with two quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.)
|- ( E. x E. y ( ph /\ ps ) <-> ( E. x E. y ph /\ ps ) )
Theorem	19.41vvv 1831*	Version of 19.41 2050 with three quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.)
|- ( E. x E. y E. z ( ph /\ ps ) <-> ( E. x E. y E. z ph /\ ps ) )
Theorem	19.41vvvv 1832*	Version of 19.41 2050 with four quantifiers and a dv condition requiring fewer axioms. (Contributed by FL, 14-Jul-2007.)
|- ( E. w E. x E. y E. z ( ph /\ ps ) <-> ( E. w E. x E. y E. z ph /\ ps ) )
Theorem	19.42v 1833*	Version of 19.42 2051 with a dv condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
|- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )
Theorem	exdistr 1834*	Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.)
|- ( E. x E. y ( ph /\ ps ) <-> E. x ( ph /\ E. y ps ) )
Theorem	19.42vv 1835*	Version of 19.42 2051 with two quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 16-Mar-1995.)
|- ( E. x E. y ( ph /\ ps ) <-> ( ph /\ E. x E. y ps ) )
Theorem	19.42vvv 1836*	Version of 19.42 2051 with three quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 21-Sep-2011.)
|- ( E. x E. y E. z ( ph /\ ps ) <-> ( ph /\ E. x E. y E. z ps ) )
Theorem	exdistr2 1837*	Distribution of existential quantifiers. (Contributed by NM, 17-Mar-1995.)
|- ( E. x E. y E. z ( ph /\ ps ) <-> E. x ( ph /\ E. y E. z ps ) )
Theorem	3exdistr 1838*	Distribution of existential quantifiers in a triple conjunction. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( E. x E. y E. z ( ph /\ ps /\ ch ) <-> E. x ( ph /\ E. y ( ps /\ E. z ch ) ) )
Theorem	4exdistr 1839*	Distribution of existential quantifiers in a quadruple conjunction. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Wolf Lammen, 20-Jan-2018.)
|- ( E. x E. y E. z E. w ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> E. x ( ph /\ E. y ( ps /\ E. z ( ch /\ E. w th ) ) ) )
Theorem	spimeh 1840*	Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Wolf Lammen, 10-Dec-2017.)
|- ( ph -> A. x ph )   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( ph -> E. x ps )
Theorem	spimw 1841*	Specialization. Lemma 8 of [KalishMontague] p. 87. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 7-Aug-2017.)
|- ( -. ps -> A. x -. ps )   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	spimvw 1842*	Specialization. Lemma 8 of [KalishMontague] p. 87. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.)
|- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	spnfw 1843	Weak version of sp 1936. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 13-Aug-2017.)
|- ( -. ph -> A. x -. ph )   =>    |- ( A. x ph -> ph )
Theorem	spfalw 1844	Version of sp 1936 when ph is false. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.) (Proof shortened by Wolf Lammen, 25-Dec-2017.)
|- -. ph   =>    |- ( A. x ph -> ph )
Theorem	equs4v 1845*	Version of equs4 2126 with a dv condition, which requires fewer axioms. (Contributed by BJ, 31-May-2019.)
|- ( A. x ( x = y -> ph ) -> E. x ( x = y /\ ph ) )
Theorem	equsalvw 1846*	Version of equsal 2127 with two dv conditions, which requires fewer axioms. (Contributed by BJ, 31-May-2019.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ( x = y -> ph ) <-> ps )
Theorem	equsexvw 1847*	Version of equsexv 2065 with a dv condition, which requires fewer axioms. See also equsex 2129. (Contributed by BJ, 31-May-2019.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ( x = y /\ ph ) <-> ps )
Theorem	cbvaliw 1848*	Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by NM, 19-Apr-2017.)
|- ( A. x ph -> A. y A. x ph )   &    |- ( -. ps -> A. x -. ps )   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> A. y ps )
Theorem	cbvalivw 1849*	Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by NM, 9-Apr-2017.)
|- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> A. y ps )
1.4.8  Axiom scheme ax-7 (Equality)
Axiom	ax-7 1850	Axiom of Equality. One of the equality and substitution axioms of predicate calculus with equality. It states that equality is right-Euclidean (this is similar, but not identical, to being transitive, which is proved as equtr 1864). 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 1527 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 1859 that this axiom can be recovered from its weakened version ax7v 1851 where x and y are assumed to be disjoint variables. In particular, the only theorem referencing ax-7 1850 should be ax7v 1851. See the comment of ax7v 1851 for more details on these matters. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 7-Dec-2020.) Use ax7 1859 instead. (New usage is discouraged.)
|- ( x = y -> ( x = z -> y = z ) )
Theorem	ax7v 1851*	Weakened version of ax-7 1850, with a dv condition on x , y. This should be the only proof referencing ax-7 1850, and it should be referenced only by its two weakened versions ax7v1 1852 and ax7v2 1853, from which ax-7 1850 is then rederived as ax7 1859, which shows that either ax7v 1851 or the conjunction of ax7v1 1852 and ax7v2 1853 is sufficient. In ax7v 1851, it is still allowed to substitute the same variable for x and z, or the same variable for y and z. Therefore, ax7v 1851 "bundles" (a term coined by Raph Levien) its "principal instance" ( x = y -> ( x = z -> y = z ) ) with x , y , z distinct, and its "degenerate instances" ( x = y -> ( x = x -> y = x ) ) and ( x = y -> ( x = y -> y = y ) ) with x , y distinct. These degenerate instances are for instance used in the proofs of equcomiv 1857 and equid 1854 respectively. (Contributed by BJ, 7-Dec-2020.) Use ax7 1859 instead. (New usage is discouraged.)
|- ( x = y -> ( x = z -> y = z ) )
Theorem	ax7v1 1852*	First of two weakened versions of ax7v 1851, with an extra dv condition on x , z, see comments there. (Contributed by BJ, 7-Dec-2020.)
|- ( x = y -> ( x = z -> y = z ) )
Theorem	ax7v2 1853*	Second of two weakened versions of ax7v 1851, with an extra dv condition on y , z, see comments there. (Contributed by BJ, 7-Dec-2020.)
|- ( x = y -> ( x = z -> y = z ) )
Theorem	equid 1854	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, 5-Feb-2018.) (Proof shortened by Wolf Lammen, 22-Aug-2020.)
|- x = x
Theorem	equidOLD 1855	Obsolete proof of equid 1854 as of 22-Aug-2020. (Contributed by NM, 1-Apr-2005.) (Revised by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- x = x
Theorem	nfequid 1856	Bound-variable hypothesis builder for x = x. This theorem tells us that any variable, including x, is effectively not free in x = x, even though x is technically free according to the traditional definition of free variable. (Contributed by NM, 13-Jan-2011.) (Revised by NM, 21-Aug-2017.)
|- F/ y x = x
Theorem	equcomiv 1857*	Weaker form of equcomi 1860 with a dv condition on x , y. This is an intermediate step and equcomi 1860 is fully recovered later. (Contributed by BJ, 7-Dec-2020.)
|- ( x = y -> y = x )
Theorem	ax6evr 1858*	A commuted form of ax6ev 1806. (Contributed by BJ, 7-Dec-2020.)
|- E. x y = x
Theorem	ax7 1859	Proof of ax-7 1850 from ax7v1 1852 and ax7v2 1853, proving sufficiency of the conjunction of the latter two weakened versions of ax7v 1851, which is itself a weakened version of ax-7 1850. Note that the weakened version of ax-7 1850 obtained by adding a dv condition on x , z (resp. on y , z) does not permit, together with the other axioms, to prove reflexivity (resp. symmetry). (Contributed by BJ, 7-Dec-2020.)
|- ( x = y -> ( x = z -> y = z ) )
Theorem	equcomi 1860	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.)
|- ( x = y -> y = x )
Theorem	equcom 1861	Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.)
|- ( x = y <-> y = x )
Theorem	equcomd 1862	Deduction form of equcom 1861, symmetry of equality. For the versions for classes, see eqcom 2457 and eqcomd 2456. (Contributed by BJ, 6-Oct-2019.)
|- ( ph -> x = y )   =>    |- ( ph -> y = x )
Theorem	equcoms 1863	An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 10-Jan-1993.)
|- ( x = y -> ph )   =>    |- ( y = x -> ph )
Theorem	equtr 1864	A transitive law for equality. (Contributed by NM, 23-Aug-1993.)
|- ( x = y -> ( y = z -> x = z ) )
Theorem	equtrr 1865	A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.)
|- ( x = y -> ( z = x -> z = y ) )
Theorem	equequ1 1866	An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.)
|- ( x = y -> ( x = z <-> y = z ) )
Theorem	equequ2 1867	An equivalence law for equality. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.)
|- ( x = y -> ( z = x <-> z = y ) )
Theorem	equtr2 1868	Equality is left-Euclidean. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ( x = z /\ y = z ) -> x = y )
Theorem	stdpc6 1869	One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1870.) 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.)
|- A. x x = x
Theorem	stdpc7 1870	One of the two equality axioms of standard predicate calculus, called substitutivity of equality. (The other one is stdpc6 1869.) Translated to traditional notation, it can be read: " x = y -> ( ph ( x , x ) -> ph ( x , y ) ), provided that y is free for x in ph ( x , x )." Axiom 7 of [Mendelson] p. 95. (Contributed by NM, 15-Feb-2005.)
|- ( x = y -> ( [ x / y ] ph -> ph ) )
Theorem	equviniv 1871*	A specialized version of equvini 2178 with a distinct variable restriction. (Contributed by Wolf Lammen, 8-Sep-2018.)
|- ( x = y -> E. z ( x = z /\ y = z ) )
Theorem	equvin 1872*	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. (Contributed by NM, 9-Jan-1993.) Remove dependencies on ax-10 1914, ax-13 2090. (Revised by Wolf Lammen, 10-Jun-2019.)
|- ( x = y <-> E. z ( x = z /\ z = y ) )
Theorem	ax13b 1873	An equivalence used to show two ways of expressing ax-13 2090. See the comment for ax-13 2090. (Contributed by NM, 2-May-2017.) (Proof shortened by Wolf Lammen, 26-Feb-2018.) (Revised by BJ, 15-Sep-2020.)
|- ( ( -. x = y -> ( y = z -> ph ) ) <-> ( -. x = y -> ( -. x = z -> ( y = z -> ph ) ) ) )
Theorem	spfw 1874*	Weak version of sp 1936. 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.)
|- ( -. ps -> A. x -. ps )   &    |- ( A. x ph -> A. y A. x ph )   &    |- ( -. ph -> A. y -. ph )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph -> ph )
Theorem	spw 1875*	Weak version of the specialization scheme sp 1936. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 1936 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 1936 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 1908 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 1936 are spfw 1874 (minimal distinct variable requirements), spnfw 1843 (when x is not free in -. ph), spvw 1813 (when x does not appear in ph), sptruw 1680 (when ph is true), and spfalw 1844 (when ph is false). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph -> ph )
Theorem	cbvalw 1876*	Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.)
|- ( A. x ph -> A. y A. x ph )   &    |- ( -. ps -> A. x -. ps )   &    |- ( A. y ps -> A. x A. y ps )   &    |- ( -. ph -> A. y -. ph )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph <-> A. y ps )
Theorem	cbvalvw 1877*	Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph <-> A. y ps )
Theorem	cbvexvw 1878*	Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ph <-> E. y ps )
Theorem	alcomiw 1879*	Weak version of alcom 1922. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.)
|- ( y = z -> ( ph <-> ps ) )   =>    |- ( A. x A. y ph -> A. y A. x ph )
Theorem	hbn1fw 1880*	Weak version of ax-10 1914 from which we can prove any ax-10 1914 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.)
|- ( A. x ph -> A. y A. x ph )   &    |- ( -. ps -> A. x -. ps )   &    |- ( A. y ps -> A. x A. y ps )   &    |- ( -. ph -> A. y -. ph )   &    |- ( -. A. y ps -> A. x -. A. y ps )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( -. A. x ph -> A. x -. A. x ph )
Theorem	hbn1w 1881*	Weak version of hbn1 1915. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( -. A. x ph -> A. x -. A. x ph )
Theorem	hba1w 1882*	Weak version of hba1 1977. See comments for ax10w 1902. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph -> A. x A. x ph )
Theorem	hbe1w 1883*	Weak version of hbe1 1916. See comments for ax10w 1902. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ph -> A. x E. x ph )
Theorem	hbalw 1884*	Weak version of hbal 1921. Uses only Tarski's FOL axiom schemes. Unlike hbal 1921, this theorem requires that x and y be distinct i.e. are not bundled. (Contributed by NM, 19-Apr-2017.)
|- ( x = z -> ( ph <-> ps ) )   &    |- ( ph -> A. x ph )   =>    |- ( A. y ph -> A. x A. y ph )
Theorem	cbvaev 1885*	Change bound variable in an equality with a dv condition. (Contributed by NM, 22-Jul-2015.) (Revised by BJ, 18-Jun-2019.)
|- ( A. x x = w -> A. y y = w )
1.4.9  Membership predicate
Syntax	wcel 1886	Extend wff definition to include the membership connective between classes. For a general discussion of the theory of classes, see http://us.metamath.org/mpeuni/mmset.html#class. (The purpose of introducing wff A e. B here is to allow us to express i.e. "prove" the wel 1887 of predicate calculus in terms of the wcel 1886 of set theory, so that we don't "overload" the e. connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers. The class variables A and B are introduced temporarily for the purpose of this definition but otherwise not used in predicate calculus. See df-clab 2437 for more information on the set theory usage of wcel 1886.)
wff A e. B
Theorem	wel 1887	Extend wff definition to include atomic formulas with the epsilon (membership) predicate. This is read " x is an element of y," " x is a member of y," " x belongs to y," or " y contains x." Note: The phrase " y includes x " means " x is a subset of y;" to use it also for x e. y, 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 e. (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 e. 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 1887 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 1886. This lets us avoid overloading the e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1887 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1886. Note: To see the proof steps of this syntax proof, type "show proof wel /all" in the Metamath program.) (Contributed by NM, 24-Jan-2006.)
wff x e. y
1.4.10  Axiom scheme ax-8 (Left Equality for Binary Predicate)
Axiom	ax-8 1888	Axiom of Left Equality for Binary Predicate. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. It substitutes equal variables into the left-hand side of an arbitrary binary predicate e., which we will use for the set membership relation when set theory is introduced. 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 scheme C12' in [Megill] p. 448 (p. 16 of the preprint). "Non-logical" means that the predicate is not a primitive of predicate calculus proper but instead is an extension to it. "Binary" means that the predicate has two arguments. In a system of predicate calculus with equality, like ours, equality is not usually considered to be a non-logical predicate. In systems of predicate calculus without equality, it typically would be. We prove in ax8 1892 that this axiom can be recovered from its weakened version ax8v 1889 where x and y are assumed to be disjoint variables. In particular, the only theorem referencing ax-8 1888 should be ax8v 1889. See the comment of ax8v 1889 for more details on these matters. (Contributed by NM, 30-Jun-1993.) (Revised by BJ, 7-Dec-2020.) Use ax8 1892 instead. (New usage is discouraged.)
|- ( x = y -> ( x e. z -> y e. z ) )
Theorem	ax8v 1889*	Weakened version of ax-8 1888, with a dv condition on x , y. This should be the only proof referencing ax-8 1888, and it should be referenced only by its two weakened versions ax8v1 1890 and ax8v2 1891, from which ax-8 1888 is then rederived as ax8 1892, which shows that either ax8v 1889 or the conjunction of ax8v1 1890 and ax8v2 1891 is sufficient. (Contributed by BJ, 7-Dec-2020.) Use ax8 1892 instead. (New usage is discouraged.)
|- ( x = y -> ( x e. z -> y e. z ) )
Theorem	ax8v1 1890*	First of two weakened versions of ax8v 1889, with an extra dv condition on x , z, see comments there. (Contributed by BJ, 7-Dec-2020.)
|- ( x = y -> ( x e. z -> y e. z ) )
Theorem	ax8v2 1891*	Second of two weakened versions of ax8v 1889, with an extra dv condition on y , z see comments there. (Contributed by BJ, 7-Dec-2020.)
|- ( x = y -> ( x e. z -> y e. z ) )
Theorem	ax8 1892	Proof of ax-8 1888 from ax8v1 1890 and ax8v2 1891, proving sufficiency of the conjunction of the latter two weakened versions of ax8v 1889, which is itself a weakened version of ax-8 1888. (Contributed by BJ, 7-Dec-2020.)
|- ( x = y -> ( x e. z -> y e. z ) )
Theorem	elequ1 1893	An identity law for the non-logical predicate. (Contributed by NM, 30-Jun-1993.)
|- ( x = y -> ( x e. z <-> y e. z ) )
Theorem	cleljust 1894*	When the class variables in definition df-clel 2446 are replaced with setvar variables, this theorem of predicate calculus is the result. This theorem provides part of the justification for the consistency of that definition, which "overloads" the setvar variables in wel 1887 with the class variables in wcel 1886. (Contributed by NM, 28-Jan-2004.) Revised to use equsexvw 1847 in order to remove dependencies on ax-10 1914, ax-12 1932, ax-13 2090. Note that there is no DV condition on x , y, that is, on the variables of the left-hand side. (Revised by BJ, 29-Dec-2020.)
|- ( x e. y <-> E. z ( z = x /\ z e. y ) )
1.4.11  Axiom scheme ax-9 (Right Equality for Binary Predicate)
Axiom	ax-9 1895	Axiom of Right Equality for Binary Predicate. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. It substitutes equal variables into the right-hand side of an arbitrary binary predicate e., which we will use for the set membership relation when set theory is introduced. 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 scheme C13' in [Megill] p. 448 (p. 16 of the preprint). We prove in ax9 1899 that this axiom can be recovered from its weakened version ax9v 1896 where x and y are assumed to be disjoint variables. In particular, the only theorem referencing ax-9 1895 should be ax9v 1896. See the comment of ax9v 1896 for more details on these matters. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 7-Dec-2020.) Use ax9 1899 instead. (New usage is discouraged.)
|- ( x = y -> ( z e. x -> z e. y ) )
Theorem	ax9v 1896*	Weakened version of ax-9 1895, with a dv condition on x , y. This should be the only proof referencing ax-9 1895, and it should be referenced only by its two weakened versions ax9v1 1897 and ax9v2 1898, from which ax-9 1895 is then rederived as ax9 1899, which shows that either ax9v 1896 or the conjunction of ax9v1 1897 and ax9v2 1898 is sufficient. (Contributed by BJ, 7-Dec-2020.) Use ax9 1899 instead. (New usage is discouraged.)
|- ( x = y -> ( z e. x -> z e. y ) )
Theorem	ax9v1 1897*	First of two weakened versions of ax9v 1896, with an extra dv condition on y , z, see comments there. (Contributed by BJ, 7-Dec-2020.)
|- ( x = y -> ( z e. x -> z e. y ) )
Theorem	ax9v2 1898*	Second of two weakened versions of ax9v 1896, with an extra dv condition on y , z see comments there. (Contributed by BJ, 7-Dec-2020.)
|- ( x = y -> ( z e. x -> z e. y ) )
Theorem	ax9 1899	Proof of ax-9 1895 from ax9v1 1897 and ax9v2 1898, proving sufficiency of the conjunction of the latter two weakened versions of ax9v 1896, which is itself a weakened version of ax-9 1895. (Contributed by BJ, 7-Dec-2020.)
|- ( x = y -> ( z e. x -> z e. y ) )
Theorem	elequ2 1900	An identity law for the non-logical predicate. (Contributed by NM, 21-Jun-1993.)
|- ( x = y -> ( z e. x <-> z e. y ) )