P. 334 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33301-33400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wl-nanbi2 33301	Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) (Revised by Wolf Lammen, 27-Jun-2020.)
|- ( ( ph <-> ps ) -> ( ( ph -/\ ch ) <-> ( ps -/\ ch ) ) )
Theorem	wl-naev 33302*	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.)
|- ( -. A. x x = y -> -. A. u u = v )
Theorem	wl-hbae1 33303	This specialization of hbae 2315 does not depend on ax-11 2034. (Contributed by Wolf Lammen, 8-Aug-2021.)
|- ( A. x x = y -> A. y A. x x = y )
Theorem	wl-naevhba1v 33304*	An instance of hbn1w 1973 applied to equality. (Contributed by Wolf Lammen, 7-Apr-2021.)
|- ( -. A. x x = y -> A. x -. A. x x = y )
Theorem	wl-hbnaev 33305*	Any variable is free in -. A. x x = y, if x and y are distinct. The latter condition can actually be lifted, but this version is easier to prove. The proof does not use ax-10 2019. (Contributed by Wolf Lammen, 9-Apr-2021.)
|- ( -. A. x x = y -> A. z -. A. x x = y )
Theorem	wl-spae 33306	Prove an instance of sp 2053 from ax-13 2246 and Tarski's FOL only, without distinct variable conditions. The antecedent A. x x = y holds in a multi-object universe only if y is substituted for x, or vice versa, i.e. both variables are effectively the same. The converse -. A. x x = y indicates that both variables are distinct, and it so provides a simple translation of a distinct variable condition to a logical term. In case studies A. x x = y and -. A. x x = y can help eliminating distinct variable conditions. The antecedent A. x x = y is expressed in the theorem's name by the abbreviation ae standing for 'all equal'. Note that we cannot provide a logical predicate telling us directly whether a logical expression contains a particular variable, as such a construct would usually contradict ax-12 2047. Note that this theorem is also provable from ax-12 2047 alone, so you can pick the axiom it is based on. Compare this result to 19.3v 1897 and spaev 1978 having distinct variable conditions, but a smaller footprint on axiom usage. (Contributed by Wolf Lammen, 5-Apr-2021.)
|- ( A. x x = y -> x = y )
Theorem	wl-cbv3vv 33307*	Avoiding ax-11 2034. (Contributed by Wolf Lammen, 30-Aug-2021.)
|- F/ x ps   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ph -> A. y ps )
Theorem	wl-speqv 33308*	Under the assumption -. x = y a specialized version of sp 2053 is provable from Tarski's FOL and ax13v 2247 only. Note that this reverts the implication in ax13lem1 2248, so in fact ( -. x = y -> ( A. x z = y <-> z = y ) ) holds. (Contributed by Wolf Lammen, 17-Apr-2021.)
|- ( -. x = y -> ( A. x z = y -> z = y ) )
Theorem	wl-19.8eqv 33309*	Under the assumption -. x = y a specialized version of 19.8a 2052 is provable from Tarski's FOL and ax13v 2247 only. Note that this reverts the implication in ax13lem2 2296, so in fact ( -. x = y -> ( E. x z = y <-> z = y ) ) holds. (Contributed by Wolf Lammen, 17-Apr-2021.)
|- ( -. x = y -> ( z = y -> E. x z = y ) )
Theorem	wl-19.2reqv 33310*	Under the assumption -. x = y the reverse direction of 19.2 1892 is provable from Tarski's FOL and ax13v 2247 only. Note that in conjunction with 19.2 1892 in fact ( -. x = y -> ( A. x z = y <-> E. x z = y ) ) holds. (Contributed by Wolf Lammen, 17-Apr-2021.)
|- ( -. x = y -> ( E. x z = y -> A. x z = y ) )
Theorem	wl-dveeq12 33311*	The current form of ax-13 2246 has a particular disadvantage: The condition -. x = y is less versatile than the general form -. A. x x = y. You need ax-10 2019 to arrive at the more general form presented here. You need 19.8a 2052 (or ax-12 2047) to restore y = z from E. x y = z again. (Contributed by Wolf Lammen, 9-Jun-2021.)
|- ( -. A. x x = y -> ( E. x z = y -> A. x z = y ) )
Theorem	wl-nfalv 33312*	If x is not present in ph, it is not free in A. y ph. (Contributed by Wolf Lammen, 11-Jan-2020.)
|- F/ x A. y ph
Theorem	wl-nfimf1 33313	An antecedent is irrelevant to a not-free property, if it always holds. I used this variant of nfim 1825 in dvelimdf 2335 to simplify the proof. (Contributed by Wolf Lammen, 14-Oct-2018.)
|- ( A. x ph -> ( F/ x ( ph -> ps ) <-> F/ x ps ) )
Theorem	wl-nfnbi 33314	Being free does not depend on an outside negation in an expression. This theorem is slightly more general than nfn 1784 or nfnd 1785. (Contributed by Wolf Lammen, 5-May-2018.)
|- ( F/ x ph <-> F/ x -. ph )
Theorem	wl-nfae1 33315	Unlike nfae 2316, this specialized theorem avoids ax-11 2034. (Contributed by Wolf Lammen, 26-Jun-2019.)
|- F/ x A. y y = x
Theorem	wl-nfnae1 33316	Unlike nfnae 2318, this specialized theorem avoids ax-11 2034. (Contributed by Wolf Lammen, 27-Jun-2019.)
|- F/ x -. A. y y = x
Theorem	wl-aetr 33317	A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019.)
|- ( A. x x = y -> ( A. x x = z -> A. y y = z ) )
Theorem	wl-dral1d 33318	A version of dral1 2325 with a context. Note: At first glance one might be tempted to generalize this (or a similar) theorem by weakening the first two hypotheses adding a x = y, A. x x = y or ph antecedent. wl-equsal1i 33329 and nf5di 2119 show that this is in fact pointless. (Contributed by Wolf Lammen, 28-Jul-2019.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ph -> ( x = y -> ( ps <-> ch ) ) )   =>    |- ( ph -> ( A. x x = y -> ( A. x ps <-> A. y ch ) ) )
Theorem	wl-cbvalnaed 33319	wl-cbvalnae 33320 with a context. (Contributed by Wolf Lammen, 28-Jul-2019.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ph -> ( -. A. x x = y -> F/ y ps ) )   &    |- ( ph -> ( -. A. x x = y -> F/ x ch ) )   &    |- ( ph -> ( x = y -> ( ps <-> ch ) ) )   =>    |- ( ph -> ( A. x ps <-> A. y ch ) )
Theorem	wl-cbvalnae 33320	A more general version of cbval 2271 when non-free properties depend on a distinctor. Such expressions arise in proofs aiming at the elimination of distinct variable constraints, specifically in application of dvelimf 2334, nfsb2 2360 or dveeq1 2300. (Contributed by Wolf Lammen, 4-Jun-2019.)
|- ( -. A. x x = y -> F/ y ph )   &    |- ( -. A. x x = y -> F/ x ps )   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph <-> A. y ps )
Theorem	wl-exeq 33321	The semantics of E. x y = z. (Contributed by Wolf Lammen, 27-Apr-2018.)
|- ( E. x y = z <-> ( y = z \/ A. x x = y \/ A. x x = z ) )
Theorem	wl-aleq 33322	The semantics of A. x y = z. (Contributed by Wolf Lammen, 27-Apr-2018.)
|- ( A. x y = z <-> ( y = z /\ ( A. x x = y <-> A. x x = z ) ) )
Theorem	wl-nfeqfb 33323	Extend nfeqf 2301 to an equivalence. (Contributed by Wolf Lammen, 31-Jul-2019.)
|- ( F/ x y = z <-> ( A. x x = y <-> A. x x = z ) )
Theorem	wl-nfs1t 33324	If y is not free in ph, x is not free in [ y / x ] ph. Closed form of nfs1 2365. (Contributed by Wolf Lammen, 27-Jul-2019.)
|- ( F/ y ph -> F/ x [ y / x ] ph )
Theorem	wl-equsald 33325	Deduction version of equsal 2291. (Contributed by Wolf Lammen, 27-Jul-2019.)
|- F/ x ph   &    |- ( ph -> F/ x ch )   &    |- ( ph -> ( x = y -> ( ps <-> ch ) ) )   =>    |- ( ph -> ( A. x ( x = y -> ps ) <-> ch ) )
Theorem	wl-equsal 33326	A useful equivalence related to substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 3-Oct-2016.) It seems proving wl-equsald 33325 first, and then deriving more specialized versions wl-equsal 33326 and wl-equsal1t 33327 then is more efficient than the other way round, which is possible, too. See also equsal 2291. (Revised by Wolf Lammen, 27-Jul-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ( x = y -> ph ) <-> ps )
Theorem	wl-equsal1t 33327	The expression x = y in antecedent position plays an important role in predicate logic, namely in implicit substitution. However, occasionally it is irrelevant, and can safely be dropped. A sufficient condition for this is when x (or y or both) is not free in ph. This theorem is more fundamental than equsal 2291, spimt 2253 or sbft 2379, to which it is related. (Contributed by Wolf Lammen, 19-Aug-2018.)
|- ( F/ x ph -> ( A. x ( x = y -> ph ) <-> ph ) )
Theorem	wl-equsalcom 33328	This simple equivalence eases substitution of one expression for the other. (Contributed by Wolf Lammen, 1-Sep-2018.)
|- ( A. x ( x = y -> ph ) <-> A. x ( y = x -> ph ) )
Theorem	wl-equsal1i 33329	The antecedent x = y is irrelevant, if one or both setvar variables are not free in ph. (Contributed by Wolf Lammen, 1-Sep-2018.)
|- ( F/ x ph \/ F/ y ph )   &    |- ( x = y -> ph )   =>    |- ph
Theorem	wl-sb6rft 33330	A specialization of wl-equsal1t 33327. Closed form of sb6rf 2423. (Contributed by Wolf Lammen, 27-Jul-2019.)
|- ( F/ x ph -> ( ph <-> A. x ( x = y -> [ x / y ] ph ) ) )
Theorem	wl-sbrimt 33331	Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim 2396. (Contributed by Wolf Lammen, 26-Jul-2019.)
|- ( F/ x ph -> ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) ) )
Theorem	wl-sblimt 33332	Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim 2396. (Contributed by Wolf Lammen, 26-Jul-2019.)
|- ( F/ x ps -> ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> ps ) ) )
Theorem	wl-sb8t 33333	Substitution of variable in universal quantifier. Closed form of sb8 2424. (Contributed by Wolf Lammen, 27-Jul-2019.)
|- ( A. x F/ y ph -> ( A. x ph <-> A. y [ y / x ] ph ) )
Theorem	wl-sb8et 33334	Substitution of variable in universal quantifier. Closed form of sb8e 2425. (Contributed by Wolf Lammen, 27-Jul-2019.)
|- ( A. x F/ y ph -> ( E. x ph <-> E. y [ y / x ] ph ) )
Theorem	wl-sbhbt 33335	Closed form of sbhb 2438. Characterizing the expression ph -> A. x ph using a substitution expression. (Contributed by Wolf Lammen, 28-Jul-2019.)
|- ( A. x F/ y ph -> ( ( ph -> A. x ph ) <-> A. y ( ph -> [ y / x ] ph ) ) )
Theorem	wl-sbnf1 33336	Two ways expressing that x is effectively not free in ph. Simplified version of sbnf2 2439. Note: This theorem shows that sbnf2 2439 has unnecessary distinct variable constraints. (Contributed by Wolf Lammen, 28-Jul-2019.)
|- ( A. x F/ y ph -> ( F/ x ph <-> A. x A. y ( ph -> [ y / x ] ph ) ) )
Theorem	wl-equsb3 33337	equsb3 2432 with a distinctor. (Contributed by Wolf Lammen, 27-Jun-2019.)
|- ( -. A. y y = z -> ( [ x / y ] y = z <-> x = z ) )
Theorem	wl-equsb4 33338	Substitution applied to an atomic wff. The distinctor antecedent is more general than a distinct variable constraint. (Contributed by Wolf Lammen, 26-Jun-2019.)
|- ( -. A. x x = z -> ( [ y / x ] y = z <-> y = z ) )
Theorem	wl-sb6nae 33339	Version of sb6 2429 suitable for elimination of unnecessary dv restrictions. (Contributed by Wolf Lammen, 28-Jul-2019.)
|- ( -. A. x x = y -> ( [ y / x ] ph <-> A. x ( x = y -> ph ) ) )
Theorem	wl-sb5nae 33340	Version of sb5 2430 suitable for elimination of unnecessary dv restrictions. (Contributed by Wolf Lammen, 28-Jul-2019.)
|- ( -. A. x x = y -> ( [ y / x ] ph <-> E. x ( x = y /\ ph ) ) )
Theorem	wl-2sb6d 33341	Version of 2sb6 2444 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.)
|- ( ph -> -. A. y y = x )   &    |- ( ph -> -. A. y y = w )   &    |- ( ph -> -. A. y y = z )   &    |- ( ph -> -. A. x x = z )   =>    |- ( ph -> ( [ z / x ] [ w / y ] ps <-> A. x A. y ( ( x = z /\ y = w ) -> ps ) ) )
Theorem	wl-sbcom2d-lem1 33342*	Lemma used to prove wl-sbcom2d 33344. (Contributed by Wolf Lammen, 10-Aug-2019.) (New usage is discouraged.)
|- ( ( u = y /\ v = w ) -> ( -. A. x x = w -> ( [ u / x ] [ v / z ] ph <-> [ y / x ] [ w / z ] ph ) ) )
Theorem	wl-sbcom2d-lem2 33343*	Lemma used to prove wl-sbcom2d 33344. (Contributed by Wolf Lammen, 10-Aug-2019.) (New usage is discouraged.)
|- ( -. A. y y = x -> ( [ u / x ] [ v / y ] ph <-> A. x A. y ( ( x = u /\ y = v ) -> ph ) ) )
Theorem	wl-sbcom2d 33344	Version of sbcom2 2445 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.)
|- ( ph -> -. A. x x = w )   &    |- ( ph -> -. A. x x = z )   &    |- ( ph -> -. A. z z = y )   =>    |- ( ph -> ( [ w / z ] [ y / x ] ps <-> [ y / x ] [ w / z ] ps ) )
Theorem	wl-sbalnae 33345	A theorem used in elimination of disjoint variable restrictions by replacing them with distinctors. (Contributed by Wolf Lammen, 25-Jul-2019.)
|- ( ( -. A. x x = y /\ -. A. x x = z ) -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
Theorem	wl-sbal1 33346*	A theorem used in elimination of disjoint variable restriction on x and y by replacing it with a distinctor -. A. x x = z. (Contributed by NM, 15-May-1993.) Proof is based on wl-sbalnae 33345 now. See also sbal1 2460. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = z -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
Theorem	wl-sbal2 33347*	Move quantifier in and out of substitution. Revised to remove a distinct variable constraint. (Contributed by NM, 2-Jan-2002.) Proof is based on wl-sbalnae 33345 now. See also sbal2 2461. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = y -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
Theorem	wl-lem-exsb 33348*	This theorem provides a basic working step in proving theorems about E* or E!. (Contributed by Wolf Lammen, 3-Oct-2019.)
|- ( x = y -> ( ph <-> A. x ( x = y -> ph ) ) )
Theorem	wl-lem-nexmo 33349	This theorem provides a basic working step in proving theorems about E* or E!. (Contributed by Wolf Lammen, 3-Oct-2019.)
|- ( -. E. x ph -> A. x ( ph -> x = z ) )
Theorem	wl-lem-moexsb 33350*	The antecedent A. x ( ph -> x = z ) relates to E* x ph, but is better suited for usage in proofs. Note that no distinct variable restriction is placed on ph. This theorem provides a basic working step in proving theorems about E* or E!. (Contributed by Wolf Lammen, 3-Oct-2019.)
|- ( A. x ( ph -> x = z ) -> ( E. x ph <-> [ z / x ] ph ) )
Theorem	wl-alanbii 33351	This theorem extends alanimi 1744 to a biconditional. Recurrent usage stacks up more quantifiers. (Contributed by Wolf Lammen, 4-Oct-2019.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( A. x ph <-> ( A. x ps /\ A. x ch ) )
Theorem	wl-mo2df 33352	Version of mo2 2479 with a context and a distinctor replacing a distinct variable condition. This version should be used only to eliminate dv conditions. (Contributed by Wolf Lammen, 11-Aug-2019.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ph -> -. A. x x = y )   &    |- ( ph -> F/ y ps )   =>    |- ( ph -> ( E* x ps <-> E. y A. x ( ps -> x = y ) ) )
Theorem	wl-mo2tf 33353	Closed form of mo2 2479 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 20-Sep-2020.)
|- ( ( -. A. x x = y /\ A. x F/ y ph ) -> ( E* x ph <-> E. y A. x ( ph -> x = y ) ) )
Theorem	wl-eudf 33354	Version of df-eu 2474 with a context and a distinctor replacing a distinct variable condition. This version should be used only to eliminate dv conditions. (Contributed by Wolf Lammen, 23-Sep-2020.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ph -> -. A. x x = y )   &    |- ( ph -> F/ y ps )   =>    |- ( ph -> ( E! x ps <-> E. y A. x ( ps <-> x = y ) ) )
Theorem	wl-eutf 33355	Closed form of df-eu 2474 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 23-Sep-2020.)
|- ( ( -. A. x x = y /\ A. x F/ y ph ) -> ( E! x ph <-> E. y A. x ( ph <-> x = y ) ) )
Theorem	wl-euequ1f 33356	euequ1 2476 proved with a distinctor. (Contributed by Wolf Lammen, 23-Sep-2020.)
|- ( -. A. x x = y -> E! x x = y )
Theorem	wl-mo2t 33357*	Closed form of mo2 2479. (Contributed by Wolf Lammen, 18-Aug-2019.)
|- ( A. x F/ y ph -> ( E* x ph <-> E. y A. x ( ph -> x = y ) ) )
Theorem	wl-mo3t 33358*	Closed form of mo3 2507. (Contributed by Wolf Lammen, 18-Aug-2019.)
|- ( A. x F/ y ph -> ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
Theorem	wl-sb8eut 33359	Substitution of variable in universal quantifier. Closed form of sb8eu 2503. (Contributed by Wolf Lammen, 11-Aug-2019.)
|- ( A. x F/ y ph -> ( E! x ph <-> E! y [ y / x ] ph ) )
Theorem	wl-sb8mot 33360	Substitution of variable in universal quantifier. Closed form of sb8mo 2504. This theorem relates to wl-mo3t 33358, since replacing ph with [ y / x ] ph in the latter yields subexpressions like [ x / y ] [ y / x ] ph, which can be reduced to ph via sbft 2379 and sbco 2412. So E* x ph <-> E* y [ y / x ] ph is provable from wl-mo3t 33358 in a simple fashion, unfortunately only if x and y are known to be distinct. To avoid any hassle with distinctors, we prefer to derive this theorem independently, ignoring the close connection between both theorems. From an educational standpoint, one would assume wl-mo3t 33358 to be more fundamental, as it hints how the "at most one" objects on both sides of the biconditional correlate (they are the same), if they exist at all, and then prove this theorem from it. (Contributed by Wolf Lammen, 11-Aug-2019.)
|- ( A. x F/ y ph -> ( E* x ph <-> E* y [ y / x ] ph ) )
Axiom	ax-wl-11v 33361*	Version of ax-11 2034 with distinct variable conditions. Currently implemented as an axiom to detect unintended references to the foundational axiom ax-11 2034. It will later be converted into a theorem directly based on ax-11 2034. (Contributed by Wolf Lammen, 28-Jun-2019.)
|- ( A. x A. y ph -> A. y A. x ph )
Theorem	wl-ax11-lem1 33362	A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019.)
|- ( A. x x = y -> ( A. x x = z <-> A. y y = z ) )
Theorem	wl-ax11-lem2 33363*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
|- ( ( A. u u = y /\ -. A. x x = y ) -> A. x u = y )
Theorem	wl-ax11-lem3 33364*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
|- ( -. A. x x = y -> F/ x A. u u = y )
Theorem	wl-ax11-lem4 33365*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
|- F/ x ( A. u u = y /\ -. A. x x = y )
Theorem	wl-ax11-lem5 33366	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
|- ( A. u u = y -> ( A. u [ u / y ] ph <-> A. y ph ) )
Theorem	wl-ax11-lem6 33367*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
|- ( ( A. u u = y /\ -. A. x x = y ) -> ( A. u A. x [ u / y ] ph <-> A. x A. y ph ) )
Theorem	wl-ax11-lem7 33368	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
|- ( A. x ( -. A. x x = y /\ ph ) <-> ( -. A. x x = y /\ A. x ph ) )
Theorem	wl-ax11-lem8 33369*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
|- ( ( A. u u = y /\ -. A. x x = y ) -> ( A. u A. x [ u / y ] ph <-> A. y A. x ph ) )
Theorem	wl-ax11-lem9 33370	The easy part when x coincides with y. (Contributed by Wolf Lammen, 30-Jun-2019.)
|- ( A. x x = y -> ( A. y A. x ph <-> A. x A. y ph ) )
Theorem	wl-ax11-lem10 33371*	We now have prepared everything. The unwanted variable u is just in one place left. pm2.61 183 can be used in conjunction with wl-ax11-lem9 33370 to eliminate the second antecedent. Missing is something along the lines of ax-6 1888, so we could remove the first antecedent. But the Metamath axioms cannot accomplish this. Such a rule must reside one abstraction level higher than all others: It says that a distinctor implies a distinct variable condition on its contained setvar. This is only needed if such conditions are required, as ax-11v does. The result of this study is for me, that you cannot introduce a setvar capturing this condition, and hope to eliminate it later. (Contributed by Wolf Lammen, 30-Jun-2019.)
|- ( A. y y = u -> ( -. A. x x = y -> ( A. y A. x ph -> A. x A. y ph ) ) )
Theorem	wl-sbcom3 33372	Substituting y for x and then z for y is equivalent to substituting z for both x and y. Copy of ~? sbcom3OLD with a shortened proof. Keep this theorem for a while here because an external reference to it exists. (Contributed by Giovanni Mascellani, 8-Apr-2018.) (Proof shortened by Wolf Lammen, 15-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( [ z / y ] [ y / x ] ph <-> [ z / x ] [ z / y ] ph )
20.17.5  1. Bootstrapping classes
Syntax	wcel-wl 33373	Redefine e. in a class context to avoid overloading and syntax check errors in mmj2. This operator requires x and B distinct.
wff x e. B
Theorem	wel-wl 33374	Redefine e. in a set context to avoid syntax check errors in mmj2. x and y must be distinct. (Contributed by Wolf Lammen, 27-Nov-2021.)
wff x e. y
Syntax	wcel2-wl 33375	Redefine e. in a class context to avoid overloading and syntax check errors in mmj2. x and B may not be distinct.
wff x e. B
Theorem	wel2-wl 33376	Redefine e. in a set context to avoid syntax check errors in mmj2. It is no syntactic error to assign the same variable to x and y. (Contributed by Wolf Lammen, 27-Nov-2021.)
wff x e. y
Axiom	ax-wl-8cl 33377*	In ZFC, as presented in this document, classes are meant to be just a notational convenience, that can be reduced to pure set theory by means of df-clab 2609 (there stated in the eliminable property). That is, in an expression x e. A, the class variable A is implicitely assumed to represent an expression { z | ph } with some appropriate ph. Unfortunately, ph syntactically covers any well-formed formula (wff), including z e. A. This choice inevitably breaks the stated property. And it potentially carries over to any expression containing class variables. To fix this, a simple rule could exclude class variables at all in a class defining wff. A more elaborate rule could detect, and limit exclusion to proper classes (potentially problematic). In any case, the verification process should enforce any such rule during replacement, which it currently does not. The result is that we rely on the awareness of theorem designers to this problem. It seems, in ZFC proper classes are reduced to a few instances only, so a careful study may reveal that this limited use does not impose logical loop holes. It must be said, still, this necessary extra knowledge contradicts the general philosophy of Metamath, trying to establish certainty by a machine executable confirmation. An extension to ZFC allows classes to exist on their own. Classes are then extensions to sets, also seamlessly extending the idea of elementhood. In order to move from the general to the specific, sets presuppose classes, so classes should be introduced first. This is somewhat in opposition to the classic order of introduction of syntactic elements, but has been carried out in the past, for example by the von-Neumann theory of classes. In the context of Metamath, which is a purely text-based syntactical concept, no semantics are imposed at the very beginning on classes. Instead axioms will narrow down bit by bit how elementhood behaves in proofs, of course always with the intuitive understanding of a human in mind. One basic property of elementhood we expect is that the 'element' is replaceable with something equal to it. Or that equality is finer grained than the elementhood relation. This idea is formally expressed in terms coined 'implicit substitution' in this document: ( ( x = y ) -> ( x e. A <-> y e. A ) ). This axiom prepares this notation. Note that particular constructions of classes like that in df-clab 2609 in fact allow to prove this axiom. Can we expect to eliminate this axiom then? No, the generalizing term still refers to an unexplained subterm x e. A, so this axiom recurs in the general case. On the other hand, our axiom here stays true, even when just the existence of a class is known, as is often the case after applying the axiom of choice, without a chance to actually construct it. We provide a version of this axiom, that requires all variables to be distinct. Step by step these restrictions are lifted, in the end covering the most general term A e. B. This axiom is meant as a replacement for ax-8 1992. (Contributed by Wolf Lammen, 27-Nov-2021.)
|- ( x = y -> ( x e. A -> y e. A ) )
Theorem	wl-ax8clv1 33378*	Lifting the distinct variable constraint on x and y in ax-wl-8cl 33377. (Contributed by Wolf Lammen, 27-Nov-2021.)
|- ( x = y -> ( x e. A -> y e. A ) )
Theorem	wl-clelv2-just 33379*	Show that the definition df-wl-clelv2 33380 is conservative. (Contributed by Wolf Lammen, 27-Nov-2021.)
|- ( x e. A <-> A. u ( u = x -> u e. A ) )
Definition	df-wl-clelv2 33380*	Define the term x e. A, x in A permitted. (Contributed by Wolf Lammen, 27-Nov-2021.)
|- ( x e. A <-> A. u ( u = x -> u e. A ) )
Theorem	wl-ax8clv2 33381	Axiom ax-wl-8cl 33377 carries over to our new definition df-wl-clelv2 33380. (Contributed by Wolf Lammen, 27-Nov-2021.)
|- ( x = y -> ( x e. A -> y e. A ) )
20.18  Mathbox for Brendan Leahy
Theorem	rabiun 33382*	Abstraction restricted to an indexed union. (Contributed by Brendan Leahy, 26-Oct-2017.)
|- { x e. U_ y e. A B | ph } = U_ y e. A { x e. B | ph }
Theorem	iundif1 33383*	Indexed union of class difference with the subtrahend held constant. (Contributed by Brendan Leahy, 6-Aug-2018.)
|- U_ x e. A ( B \ C ) = ( U_ x e. A B \ C )
Theorem	imadifss 33384	The difference of images is a subset of the image of the difference. (Contributed by Brendan Leahy, 21-Aug-2020.)
|- ( ( F " A ) \ ( F " B ) ) C_ ( F " ( A \ B ) )
Theorem	cureq 33385	Equality theorem for currying. (Contributed by Brendan Leahy, 2-Jun-2021.)
|- ( A = B -> curry A = curry B )
Theorem	unceq 33386	Equality theorem for uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.)
|- ( A = B -> uncurry A = uncurry B )
Theorem	curf 33387	Functional property of currying. (Contributed by Brendan Leahy, 2-Jun-2021.)
|- ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) -> curry F : A --> ( C ^m B ) )
Theorem	uncf 33388	Functional property of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.)
|- ( F : A --> ( C ^m B ) -> uncurry F : ( A X. B ) --> C )
Theorem	curfv 33389	Value of currying. (Contributed by Brendan Leahy, 2-Jun-2021.)
|- ( ( ( F Fn ( V X. W ) /\ A e. V /\ B e. W ) /\ W e. X ) -> ( (curry F ` A ) ` B ) = ( A F B ) )
Theorem	uncov 33390	Value of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.)
|- ( ( A e. V /\ B e. W ) -> ( Auncurry F B ) = ( ( F ` A ) ` B ) )
Theorem	curunc 33391	Currying of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.)
|- ( ( F : A --> ( C ^m B ) /\ B =/= (/) ) -> curry uncurry F = F )
Theorem	unccur 33392	Uncurrying of currying. (Contributed by Brendan Leahy, 5-Jun-2021.)
|- ( ( F : ( A X. B ) --> C /\ B e. ( V \ { (/) } ) /\ C e. W ) -> uncurry curry F = F )
Theorem	phpreu 33393*	Theorem related to pigeonhole principle. (Contributed by Brendan Leahy, 21-Aug-2020.)
|- ( ( A e. Fin /\ A ~~ B ) -> ( A. x e. A E. y e. B x = C <-> A. x e. A E! y e. B x = C ) )
Theorem	finixpnum 33394*	A finite Cartesian product of numerable sets is numerable. (Contributed by Brendan Leahy, 24-Feb-2019.)
|- ( ( A e. Fin /\ A. x e. A B e. dom card ) -> X_ x e. A B e. dom card )
Theorem	fin2solem 33395*	Lemma for fin2so 33396. (Contributed by Brendan Leahy, 29-Jun-2019.)
|- ( ( R Or x /\ ( y e. x /\ z e. x ) ) -> ( y R z -> { w e. x | w R y } [ C.] { w e. x | w R z } ) )
Theorem	fin2so 33396	Any totally ordered Tarski-finite set is finite; in particular, no amorphous set can be ordered. Theorem 2 of [Levy58]] p. 4. (Contributed by Brendan Leahy, 28-Jun-2019.)
|- ( ( A e. FinII /\ R Or A ) -> A e. Fin )
Theorem	ltflcei 33397	Theorem to move the floor function across a strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( |_ ` A ) < B <-> A < -u ( |_ ` -u B ) ) )
Theorem	leceifl 33398	Theorem to move the floor function across a non-strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.)
|- ( ( A e. RR /\ B e. RR ) -> ( -u ( |_ ` -u A ) <_ B <-> A <_ ( |_ ` B ) ) )
Theorem	sin2h 33399	Half-angle rule for sine. (Contributed by Brendan Leahy, 3-Aug-2018.)
|- ( A e. ( 0 [,] ( 2 x. pi ) ) -> ( sin ` ( A / 2 ) ) = ( sqr ` ( ( 1 - ( cos ` A ) ) / 2 ) ) )
Theorem	cos2h 33400	Half-angle rule for cosine. (Contributed by Brendan Leahy, 4-Aug-2018.)
|- ( A e. ( -u pi [,] pi ) -> ( cos ` ( A / 2 ) ) = ( sqr ` ( ( 1 + ( cos ` A ) ) / 2 ) ) )