P. 20 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 1901-2000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	19.34 1901	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 1902*	Version of 19.23 2080 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 1903*	Theorem 19.23v 1902 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 1904*	Version of 19.36 2098 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 1905*	Inference associated with 19.36v 1904. Version of 19.36i 2099 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 1906*	Version of pm11.53 2179 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 1907*	Version of 19.12vv 2180 with a dv condition, requiring fewer axioms. See also 19.12 2164. (Contributed by BJ, 18-Mar-2020.)
|- ( E. x A. y ( ph -> ps ) <-> A. y E. x ( ph -> ps ) )
Theorem	19.27v 1908*	Version of 19.27 2095 with a dv condition, requiring fewer axioms. (Contributed by NM, 3-Jun-2004.)
|- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ ps ) )
Theorem	19.28v 1909*	Version of 19.28 2096 with a dv condition, requiring fewer axioms. (Contributed by NM, 25-Mar-2004.)
|- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) )
Theorem	19.37v 1910*	Version of 19.37 2100 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
|- ( E. x ( ph -> ps ) <-> ( ph -> E. x ps ) )
Theorem	19.37iv 1911*	Inference associated with 19.37v 1910. (Contributed by NM, 5-Aug-1993.)
|- E. x ( ph -> ps )   =>    |- ( ph -> E. x ps )
Theorem	19.44v 1912*	Version of 19.44 2106 with a dv condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
|- ( E. x ( ph \/ ps ) <-> ( E. x ph \/ ps ) )
Theorem	19.45v 1913*	Version of 19.45 2107 with a dv condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.)
|- ( E. x ( ph \/ ps ) <-> ( ph \/ E. x ps ) )
Theorem	19.41v 1914*	Version of 19.41 2103 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
|- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) )
Theorem	19.41vv 1915*	Version of 19.41 2103 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 1916*	Version of 19.41 2103 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 1917*	Version of 19.41 2103 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 1918*	Version of 19.42 2105 with a dv condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
|- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )
Theorem	exdistr 1919*	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 1920*	Version of 19.42 2105 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 1921*	Version of 19.42 2105 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 1922*	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 1923*	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 1924*	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 1925*	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 1926*	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 1927*	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 1928	Weak version of sp 2053. 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 1929	Version of sp 2053 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 1930*	Version of equs4 2290 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 1931*	Version of equsalv 2108 with a dv condition, and of equsal 2291 with two dv conditions, which requires fewer axioms. See also the dual form equsexvw 1932. (Contributed by BJ, 31-May-2019.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ( x = y -> ph ) <-> ps )
Theorem	equsexvw 1932*	Version of equsexv 2109 with a dv condition, and of equsex 2292 with two dv conditions, which requires fewer axioms. See also the dual form equsalvw 1931. (Contributed by BJ, 31-May-2019.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ( x = y /\ ph ) <-> ps )
Theorem	cbvaliw 1933*	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 1934*	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 1935	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 1948). 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 1943 that this axiom can be recovered from its weakened version ax7v 1936 where x and y are assumed to be disjoint variables. In particular, the only theorem referencing ax-7 1935 should be ax7v 1936. See the comment of ax7v 1936 for more details on these matters. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 7-Dec-2020.) Use ax7 1943 instead. (New usage is discouraged.)
|- ( x = y -> ( x = z -> y = z ) )
Theorem	ax7v 1936*	Weakened version of ax-7 1935, with a dv condition on x , y. This should be the only proof referencing ax-7 1935, and it should be referenced only by its two weakened versions ax7v1 1937 and ax7v2 1938, from which ax-7 1935 is then rederived as ax7 1943, which shows that either ax7v 1936 or the conjunction of ax7v1 1937 and ax7v2 1938 is sufficient. In ax7v 1936, it is still allowed to substitute the same variable for x and z, or the same variable for y and z. Therefore, ax7v 1936 "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 1941 and equid 1939 respectively. (Contributed by BJ, 7-Dec-2020.) Use ax7 1943 instead. (New usage is discouraged.)
|- ( x = y -> ( x = z -> y = z ) )
Theorem	ax7v1 1937*	First of two weakened versions of ax7v 1936, 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 1938*	Second of two weakened versions of ax7v 1936, 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 1939	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	nfequid 1940	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 1941*	Weaker form of equcomi 1944 with a dv condition on x , y. This is an intermediate step and equcomi 1944 is fully recovered later. (Contributed by BJ, 7-Dec-2020.)
|- ( x = y -> y = x )
Theorem	ax6evr 1942*	A commuted form of ax6ev 1890. (Contributed by BJ, 7-Dec-2020.)
|- E. x y = x
Theorem	ax7 1943	Proof of ax-7 1935 from ax7v1 1937 and ax7v2 1938, proving sufficiency of the conjunction of the latter two weakened versions of ax7v 1936, which is itself a weakened version of ax-7 1935. Note that the weakened version of ax-7 1935 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 1944	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 1945	Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.)
|- ( x = y <-> y = x )
Theorem	equcomd 1946	Deduction form of equcom 1945, symmetry of equality. For the versions for classes, see eqcom 2629 and eqcomd 2628. (Contributed by BJ, 6-Oct-2019.)
|- ( ph -> x = y )   =>    |- ( ph -> y = x )
Theorem	equcoms 1947	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 1948	A transitive law for equality. (Contributed by NM, 23-Aug-1993.)
|- ( x = y -> ( y = z -> x = z ) )
Theorem	equtrr 1949	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	equeuclr 1950	Commuted version of equeucl 1951 (equality is left-Euclidean). (Contributed by BJ, 12-Apr-2021.)
|- ( x = z -> ( y = z -> y = x ) )
Theorem	equeucl 1951	Equality is a left-Euclidean binary relation. (Right-Euclideanness is stated in ax-7 1935.) Curried (exported) form of equtr2 1954. (Contributed by BJ, 11-Apr-2021.)
|- ( x = z -> ( y = z -> x = y ) )
Theorem	equequ1 1952	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 1953	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.)
|- ( x = y -> ( z = x <-> z = y ) )
Theorem	equtr2 1954	Equality is a left-Euclidean binary relation. Uncurried (imported) form of equeucl 1951. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by BJ, 11-Apr-2021.)
|- ( ( x = z /\ y = z ) -> x = y )
Theorem	equequ2OLD 1955	Obsolete proof of equequ2 1953 as of 12-Apr-2021. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = y -> ( z = x <-> z = y ) )
Theorem	equtr2OLD 1956	Obsolete proof of equtr2 1954 as of 11-Apr-2021. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( x = z /\ y = z ) -> x = y )
Theorem	stdpc6 1957	One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1958.) 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 1958	One of the two equality axioms of standard predicate calculus, called substitutivity of equality. (The other one is stdpc6 1957.) 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	equvinv 1959*	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. (Contributed by NM, 9-Jan-1993.) Remove dependencies on ax-10 2019, ax-13 2246. (Revised by Wolf Lammen, 10-Jun-2019.) Move the quantified variable ( z) to the left of the equality signs. (Revised by Wolf Lammen, 11-Apr-2021.)
|- ( x = y <-> E. z ( z = x /\ z = y ) )
Theorem	equviniva 1960*	A modified version of the forward implication of equvinv 1959 adapted to common usage. (Contributed by Wolf Lammen, 8-Sep-2018.)
|- ( x = y -> E. z ( x = z /\ y = z ) )
Theorem	equvinivOLD 1961*	The forward implication of equvinv 1959. Obsolete as of 11-Apr-2021. Use equvinv 1959 instead. (Contributed by Wolf Lammen, 11-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = y -> E. z ( z = x /\ z = y ) )
Theorem	equvinvOLD 1962*	Obsolete version of equvinv 1959 as of 11-Apr-2021. (Contributed by NM, 9-Jan-1993.) Remove dependencies on ax-10 2019, ax-13 2246. (Revised by Wolf Lammen, 10-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = y <-> E. z ( x = z /\ y = z ) )
Theorem	equvelv 1963*	A specialized version of equvel 2347 with distinct variable restrictions and fewer axiom usage. (Contributed by Wolf Lammen, 10-Apr-2021.)
|- ( x = y <-> A. z ( z = x -> z = y ) )
Theorem	ax13b 1964	An equivalence between two ways of expressing ax-13 2246. See the comment for ax-13 2246. (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 1965*	Weak version of sp 2053. 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.)
|- ( -. 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	spfwOLD 1966*	Obsolete proof of spfw 1965 as of 10-Oct-2021. (Contributed by NM, 19-Apr-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. 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 1967*	Weak version of the specialization scheme sp 2053. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2053 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2053 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2012 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2053 are spfw 1965 (minimal distinct variable requirements), spnfw 1928 (when x is not free in -. ph), spvw 1898 (when x does not appear in ph), sptruw 1733 (when ph is true), and spfalw 1929 (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 1968*	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 1969*	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 1970*	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 1971*	Weak version of alcom 2037. 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 1972*	Weak version of ax-10 2019 from which we can prove any ax-10 2019 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 1973*	Weak version of hbn1 2020. 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 1974*	Weak version of hba1 2151. See comments for ax10w 2006. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 10-Oct-2021.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph -> A. x A. x ph )
Theorem	hba1wOLD 1975*	Obsolete proof of hba1w 1974 as of 10-Oct-2021. (Contributed by NM, 9-Apr-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph -> A. x A. x ph )
Theorem	hbe1w 1976*	Weak version of hbe1 2021. See comments for ax10w 2006. 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 1977*	Weak version of hbal 2036. Uses only Tarski's FOL axiom schemes. Unlike hbal 2036, this theorem requires that x and y be distinct, i.e. not be bundled. (Contributed by NM, 19-Apr-2017.)
|- ( x = z -> ( ph <-> ps ) )   &    |- ( ph -> A. x ph )   =>    |- ( A. y ph -> A. x A. y ph )
Theorem	spaev 1978*	A special instance of sp 2053 applied to an equality with a dv condition. Unlike the more general sp 2053, we can prove this without ax-12 2047. Instance of aeveq 1982. The antecedent A. x x = y with distinct x and y 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 A. x x = y is denoted by 'aev', a shorthand for 'all equal, with a distinct variable condition'. (Contributed by Wolf Lammen, 14-Mar-2021.)
|- ( A. x x = y -> x = y )
Theorem	cbvaev 1979*	Change bound variable in an equality with a dv condition. Instance of aev 1983. (Contributed by NM, 22-Jul-2015.) (Revised by BJ, 18-Jun-2019.)
|- ( A. x x = y -> A. z z = y )
Theorem	aevlem0 1980*	Lemma for aevlem 1981. Instance of aev 1983. (Contributed by NM, 8-Jul-2016.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-12 2047. (Revised by Wolf Lammen, 14-Mar-2021.) (Revised by BJ, 29-Mar-2021.) (Proof shortened by Wolf Lammen, 30-Mar-2021.)
|- ( A. x x = y -> A. z z = x )
Theorem	aevlem 1981*	Lemma for aev 1983 and axc16g 2134. Change free and bound variables. Instance of aev 1983. (Contributed by NM, 22-Jul-2015.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-13 2246, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 29-Mar-2021.)
|- ( A. x x = y -> A. z z = t )
Theorem	aeveq 1982*	The antecedent A. x x = y with a dv condition (typical of a one-object universe) forces equality of everything. (Contributed by Wolf Lammen, 19-Mar-2021.)
|- ( A. x x = y -> z = t )
Theorem	aev 1983*	A "distinctor elimination" lemma with no restrictions on variables in the consequent. (Contributed by NM, 8-Nov-2006.) Remove dependency on ax-11 2034. (Revised by Wolf Lammen, 7-Sep-2018.) Remove dependency on ax-13 2246, inspired by an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) Remove dependency on ax-12 2047. (Revised by Wolf Lammen, 19-Mar-2021.)
|- ( A. x x = y -> A. z t = u )
Theorem	hbaevg 1984*	Generalization of hbaev 1985, proved at no extra cost. Instance of aev2 1986. (Contributed by Wolf Lammen, 22-Mar-2021.) (Revised by BJ, 29-Mar-2021.)
|- ( A. x x = y -> A. z A. t t = u )
Theorem	hbaev 1985*	Version of hbae 2315 with a DV condition, requiring fewer axioms. Instance of hbaevg 1984 and aev2 1986. (Contributed by Wolf Lammen, 22-Mar-2021.)
|- ( A. x x = y -> A. z A. x x = y )
Theorem	aev2 1986*	A version of aev 1983 with two universal quantifiers in the consequent, and a generalization of hbaevg 1984. One can prove similar statements with arbitrary numbers of universal quantifiers in the consequent (the series begins with aeveq 1982, aev 1983, aev2 1986). Using aev 1983 and alrimiv 1855 (as in aev2ALT 1987), one can actually prove (with no more axioms) any scheme of the form ( A. x x = y -> PHI) , DV ( x , y ) where PHI involves only setvar variables and the connectors ->, <->, /\, \/, T., =, A., E., E*, E!, F/. An example is given by aevdemo 27317. This list cannot be extended to -. or F. since the scheme A. x x = y is consistent with ax-mp 5, ax-gen 1722, ax-1 6-- ax-13 2246 (as the one-element universe shows). (Contributed by BJ, 29-Mar-2021.)
|- ( A. x x = y -> A. z A. t u = v )
Theorem	aev2ALT 1987*	Alternate proof of aev2 1986, bypassing hbaevg 1984. (Contributed by BJ, 23-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = y -> A. z A. t u = v )
Theorem	axc11nlemOLD2 1988*	Lemma for axc11n 2307. Change bound variable in an equality. Obsolete as of 29-Mar-2021. Use aev 1983 instead. (Contributed by NM, 8-Jul-2016.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Restructure to ease either bundling, or reducing dependencies on axioms. (Revised by Wolf Lammen, 30-Nov-2019.) Remove dependency on ax-12 2047. (Revised by Wolf Lammen, 14-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. y y = x -> ( x = z -> A. y x = z ) )   =>    |- ( A. x x = z -> A. y y = x )
Theorem	aevlemOLD 1989*	Old proof of aevlem 1981. Obsolete as of 29-Mar-2021. (Contributed by NM, 22-Jul-2015.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-13 2246, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. z z = w -> A. y y = x )
1.4.9  Membership predicate
Syntax	wcel 1990	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 A e. B here is to allow us to express i.e. "prove" the wel 1991 of predicate calculus in terms of the wcel 1990 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 2609 for more information on the set theory usage of wcel 1990.)
wff A e. B
Theorem	wel 1991	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 1991 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 1990. This lets us avoid overloading the e. connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1991 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1990. 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 1992	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 1996 that this axiom can be recovered from its weakened version ax8v 1993 where x and y are assumed to be disjoint variables. In particular, the only theorem referencing ax-8 1992 should be ax8v 1993. See the comment of ax8v 1993 for more details on these matters. (Contributed by NM, 30-Jun-1993.) (Revised by BJ, 7-Dec-2020.) Use ax8 1996 instead. (New usage is discouraged.)
|- ( x = y -> ( x e. z -> y e. z ) )
Theorem	ax8v 1993*	Weakened version of ax-8 1992, with a dv condition on x , y. This should be the only proof referencing ax-8 1992, and it should be referenced only by its two weakened versions ax8v1 1994 and ax8v2 1995, from which ax-8 1992 is then rederived as ax8 1996, which shows that either ax8v 1993 or the conjunction of ax8v1 1994 and ax8v2 1995 is sufficient. (Contributed by BJ, 7-Dec-2020.) Use ax8 1996 instead. (New usage is discouraged.)
|- ( x = y -> ( x e. z -> y e. z ) )
Theorem	ax8v1 1994*	First of two weakened versions of ax8v 1993, 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 1995*	Second of two weakened versions of ax8v 1993, 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 1996	Proof of ax-8 1992 from ax8v1 1994 and ax8v2 1995, proving sufficiency of the conjunction of the latter two weakened versions of ax8v 1993, which is itself a weakened version of ax-8 1992. (Contributed by BJ, 7-Dec-2020.) (Proof shortened by Wolf Lammen, 11-Apr-2021.)
|- ( x = y -> ( x e. z -> y e. z ) )
Theorem	elequ1 1997	An identity law for the non-logical predicate. (Contributed by NM, 30-Jun-1993.)
|- ( x = y -> ( x e. z <-> y e. z ) )
Theorem	cleljust 1998*	When the class variables in definition df-clel 2618 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 1991 with the class variables in wcel 1990. (Contributed by NM, 28-Jan-2004.) Revised to use equsexvw 1932 in order to remove dependencies on ax-10 2019, ax-12 2047, ax-13 2246. 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 1999	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 2003 that this axiom can be recovered from its weakened version ax9v 2000 where x and y are assumed to be disjoint variables. In particular, the only theorem referencing ax-9 1999 should be ax9v 2000. See the comment of ax9v 2000 for more details on these matters. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 7-Dec-2020.) Use ax9 2003 instead. (New usage is discouraged.)
|- ( x = y -> ( z e. x -> z e. y ) )
Theorem	ax9v 2000*	Weakened version of ax-9 1999, with a dv condition on x , y. This should be the only proof referencing ax-9 1999, and it should be referenced only by its two weakened versions ax9v1 2001 and ax9v2 2002, from which ax-9 1999 is then rederived as ax9 2003, which shows that either ax9v 2000 or the conjunction of ax9v1 2001 and ax9v2 2002 is sufficient. (Contributed by BJ, 7-Dec-2020.) Use ax9 2003 instead. (New usage is discouraged.)
|- ( x = y -> ( z e. x -> z e. y ) )