P. 338 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33701-33800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-19.21t 33701	Proof of 19.21t 1852 from stdpc5t 33698. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
|- ( F/ x ph -> ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) ) )
Theorem	exlimii 33702	Inference associated with exlimi 1859. Inferring a theorem when it is implied by an antecedent which may be true. (Contributed by BJ, 15-Sep-2018.)
|- F/ x ps   &    |- ( ph -> ps )   &    |- E. x ph   =>    |- ps
Theorem	ax11-pm 33703	Proof of ax-11 1791 similar to PM's proof of alcom 1794 (PM*11.2). For a proof closer to PM's proof, see ax11-pm2 33707. Axiom ax-11 1791 is used in the proof only through nfa2 1900. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
|- ( A. x A. y ph -> A. y A. x ph )
Theorem	ax6er 33704	Another form of ax6e 1971. ( Could be placed right after ax6e 1971). (Contributed by BJ, 15-Sep-2018.)
|- E. x y = x
Theorem	exlimiieq1 33705	Inferring a theorem when it is implied by an equality which may be true. (Contributed by BJ, 30-Sep-2018.)
|- F/ x ph   &    |- ( x = y -> ph )   =>    |- ph
Theorem	exlimiieq2 33706	Inferring a theorem when it is implied by an equality which may be true. (Contributed by BJ, 15-Sep-2018.) (Revised by BJ, 30-Sep-2018.)
|- F/ y ph   &    |- ( x = y -> ph )   =>    |- ph
Theorem	ax11-pm2 33707*	Proof of ax-11 1791 from the standard axioms of predicate calculus, similar to PM's proof of alcom 1794 (PM*11.2). This proof requires that x and y be distinct. Axiom ax-11 1791 is used in the proof only through nfal 1894, nfsb 2168, sbal 2196, sb8 2147. See also ax11-pm 33703. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
|- ( A. x A. y ph -> A. y A. x ph )
21.29.4.17  Lemmas for substitution
Theorem	bj-sbf3 33708	Substitution has no effect on a bound variabe (existential quantifier case); see sbf2 2096. (Contributed by BJ, 2-May-2019.)
|- ( [ y / x ] E. x ph <-> E. x ph )
Theorem	bj-sbf4 33709	Substitution has no effect on a bound variabe (non-freeness case); see sbf2 2096. (Contributed by BJ, 2-May-2019.)
|- ( [ y / x ] F/ x ph <-> F/ x ph )
Theorem	bj-sbnf 33710*	Move non-free predicate in and out of substitution; see sbal 2196 and sbex 2198. (Contributed by BJ, 2-May-2019.)
|- ( [ z / y ] F/ x ph <-> F/ x [ z / y ] ph )
21.29.4.18  Existential uniqueness
Theorem	bj-eu3f 33711*	Version of eu3v 2307 where the dv condition is replaced with a non-freeness hypothesis. This is a "backup" of a theorem that used to be in the main part with label "eu3" and was deprecated in favor of eu3v 2307. (Contributed by NM, 8-Jul-1994.) (Proof shortened by BJ, 31-May-2019.)
|- F/ y ph   =>    |- ( E! x ph <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) )
Theorem	bj-eumo0 33712*	Existential uniqueness implies "at most one." Used to be in the main part and deprecated in favor of eumo 2308 and mo2 2287. (Contributed by NM, 8-Jul-1994.) (Revised by BJ, 8-Jun-2019.)
|- F/ y ph   =>    |- ( E! x ph -> E. y A. x ( ph -> x = y ) )
21.29.5  Set theory
21.29.5.1  Eliminability of class terms In this section, we give a sketch of the proof of the Eliminability Theorem for class terms in an extensional set theory where quantification occurs only over set variables. Eliminability of class variables using the $a-statements ax-ext 2445, df-clab 2453, df-cleq 2459, df-clel 2462 is an easy result, proved for instance in Appendix X of Azriel Levy, Basic Set Theory, Dover Publications, 2002. Note that viewed from the set.mm axiomatization, it is a metatheorem not formalizable is set.mm. It states: every formula in the language of FOL + e. + class terms, but without class variables is provably equivalent (over {FOL, ax-ext 2445, df-clab 2453, df-cleq 2459, df-clel 2462 }) to a formula in the language of FOL + e. (that is, without class terms). The proof goes by induction on the complexity of the formula (see op. cit. for details). The base case is that of atomic formulas. The atomic formulas containing class terms are of one of the following forms: for equality, x = { y | ph }, { x | ph } = y, { x | ph } = { y | ps }, and for membership, y e. { x | ph }, { x | ph } e. y, { x | ph } e. { y | ps }. These cases are dealt with by eliminable1 33713 and the following theorems of this section, which are special instances of df-clab 2453, dfcleq 2460 (proved from {FOL, ax-ext 2445, df-cleq 2459 }), and df-clel 2462. Indeed, denote by (i) the formula proved by "eliminablei". One sees that the RHS of (1) has no class terms, the RHS's of (2x) have only class terms of the form dealt with by (1), and the RHS's of (3x) have only class terms of the forms dealt with by (1) and (2a). Note that in order to prove eliminable2a 33714, eliminable2b 33715 and eliminable3a 33717, we need to substitute a class variable for a setvar variable. This is possible because setvars are class terms: this is the content of the syntactic theorem cv 1378, which is used in these proofs (this does not appear in the html pages but it is in the set.mm file and you can check it using the Metamath program). The induction step relies on the fact that any formula is a FOL-combination of atomic formulas, so if one found equivalents for all atomic formulas constituting the formula, then the same FOL-combination of these equivalents will be equivalent to the original formula. Note that one has a slightly more precise result: if the original formula has only class terms appearing in atomic formulas of the form y e. { x | ph }, then df-clab 2453 is sufficient (over FOL) to eliminate class terms, and if the original formula has only class terms appearing in atomic formulas of the form y e. { x | ph } and equalities, then df-clab 2453, ax-ext 2445 and df-cleq 2459 are sufficient (over FOL) to eliminate class terms. To prove that { df-clab 2453, df-cleq 2459, df-clel 2462 } provides a definitional extension of {FOL, ax-ext 2445 }, one needs to prove the above Eliminability Theorem, which compares the expressive powers of the languages with and without class terms, and the Conservativity Theorem, which compares the deductive powers when one adds { df-clab 2453, df-cleq 2459, df-clel 2462 }. It states that a formula without class terms is provable in one axiom system if and only if it is provable in the other, and that this remains true when one adds further definitions to {FOL, ax-ext 2445 } . It is also proved in op. cit. The proof is more difficult, since one has to construct for each proof of a statement without class terms, an associated proof not using { df-clab 2453, df-cleq 2459, df-clel 2462 }. It involves a careful case study on the structure of the proof tree.
Theorem	eliminable1 33713	A theorem used to prove the base case of the Eliminability Theorem (see section comment). (Contributed by BJ, 19-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( y e. { x | ph } <-> [ y / x ] ph )
Theorem	eliminable2a 33714*	A theorem used to prove the base case of the Eliminability Theorem (see section comment). (Contributed by BJ, 19-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = { y | ph } <-> A. z ( z e. x <-> z e. { y | ph } ) )
Theorem	eliminable2b 33715*	A theorem used to prove the base case of the Eliminability Theorem (see section comment). (Contributed by BJ, 19-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( { x | ph } = y <-> A. z ( z e. { x | ph } <-> z e. y ) )
Theorem	eliminable2c 33716*	A theorem used to prove the base case of the Eliminability Theorem (see section comment). (Contributed by BJ, 19-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( { x | ph } = { y | ps } <-> A. z ( z e. { x | ph } <-> z e. { y | ps } ) )
Theorem	eliminable3a 33717*	A theorem used to prove the base case of the Eliminability Theorem (see section comment). (Contributed by BJ, 19-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( { x | ph } e. y <-> E. z ( z = { x | ph } /\ z e. y ) )
Theorem	eliminable3b 33718*	A theorem used to prove the base case of the Eliminability Theorem (see section comment). (Contributed by BJ, 19-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( { x | ph } e. { y | ps } <-> E. z ( z = { x | ph } /\ z e. { y | ps } ) )
Theorem	bj-termab 33719*	Every class can be written as (is equal to) a class abstraction. cvjust 2461 is a special instance of it, but the present proof does not require ax-13 1968, contrary to cvjust 2461. This theorem requires ax-ext 2445, df-clab 2453, df-cleq 2459, df-clel 2462, but to prove that any specific class term not containing class variables is a setvar or can be written as (is equal to) a class abstraction does not require these $a-statements. This last fact is a metatheorem, consequence of the fact that the only $a-statements with typecode class are cv 1378, cab 2452 and statements corresponding to defined class constructors. UPDATE: it is (almost) abid2 2607 and bj-abid2 33666, though the present proof is shorter than a proof from bj-abid2 33666 and eqcomi 2480 (and is shorter than the proof of either) ; plus, it is of the same form as cvjust 2461 and such a basic statement deserves to be present in both forms. Note that bj-termab 33719 shortens the proof of abid2 2607, and shortens five proofs by a total of 72 bytes. Move it to main as "abid1"? (Contributed by BJ, 21-Oct-2019.) (Proof modification is discouraged.)
|- A = { x | x e. A }
21.29.5.2  Classes without extensionality A few results about classes can be proved without using ax-ext 2445. One could move all theorems from cab 2452 to df-clel 2462 (except for dfcleq 2460 and cvjust 2461) in a subsection "Classes" before the subsection on the axiom of extensionality, together with the theorems below. In that subsection, the last statement should be df-cleq 2459. Note that without ax-ext 2445, the $a-statements df-clab 2453, df-cleq 2459, and df-clel 2462 are no longer eliminable (see previous section) (but PROBABLY are still conservative). This is not a reason not to study what is provable with them but without ax-ext 2445, in order to gauge their strengths more precisely. Before that subsection, a subsection "The membership predicate" could group the statements with e. that are currently in the FOL part (including wcel 1767, wel 1768, ax-8 1769, ax-9 1771).
Theorem	bj-eleq1w 33720	Weaker version of eleq1 2539 (but more general than elequ1 1770) not depending on ax-ext 2445 (nor ax-12 1803 nor df-cleq 2459). Remark: this can also be done with eleq1i 2544, eqeltri 2551, eqeltrri 2552, eleq1a 2550, eleq1d 2536, eqeltrd 2555, eqeltrrd 2556, eqneltrd 2576, eqneltrrd 2577, nelneq 2584. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( x e. A <-> y e. A ) )
Theorem	bj-eleq2w 33721	Weaker version of eleq2 2540 (but more general than elequ2 1772) not depending on ax-ext 2445 (nor ax-12 1803 nor df-cleq 2459). (Contributed by BJ, 29-Sep-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( A e. x <-> A e. y ) )
Theorem	bj-clelsb3 33722*	Remove dependency on ax-ext 2445 (and df-cleq 2459) from clelsb3 2588. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( [ x / y ] y e. A <-> x e. A )
Theorem	bj-hblem 33723*	Remove dependency on ax-ext 2445 (and df-cleq 2459) from hblem 2590. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( y e. A -> A. x y e. A )   =>    |- ( z e. A -> A. x z e. A )
Theorem	bj-nfcjust 33724*	Remove dependency on ax-ext 2445 (and df-cleq 2459 and ax-13 1968) from nfcjust 2616. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( A. y F/ x y e. A <-> A. z F/ x z e. A )
Theorem	bj-nfcrii 33725*	Remove dependency on ax-ext 2445 (and df-cleq 2459) from nfcrii 2621. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- F/_ x A   =>    |- ( y e. A -> A. x y e. A )
Theorem	bj-nfcri 33726*	Remove dependency on ax-ext 2445 (and df-cleq 2459) from nfcri 2622. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- F/_ x A   =>    |- F/ x y e. A
Theorem	bj-nfnfc 33727	Remove dependency on ax-ext 2445 (and df-cleq 2459) from nfnfc 2638. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- F/_ x A   =>    |- F/ x F/_ y A
Theorem	bj-vexwt 33728	Closed form of bj-vexw 33729. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) Use bj-vexwvt 33730 instead when sufficient. (New usage is discouraged.)
|- ( A. x ph -> y e. { x | ph } )
Theorem	bj-vexw 33729	If ph is a theorem, then any set belongs to the class { x | ph }. Therefore, { x | ph } is "a" universal class. This is the closest one can get to defining a universal class, or proving vex 3116, without using ax-ext 2445. Note that this theorem has no dv condition and does not use df-clel 2462 nor df-cleq 2459 either: only first-order logic and df-clab 2453. Without ax-ext 2445, one cannot define "the" universal class, since one could not prove for instance the justification theorem { x | T. } = { y | T. }. Indeed, in order to prove any equality of classes, one needs df-cleq 2459, which has ax-ext 2445 as a hypothesis. Therefore, the classes { x | T. }, { y | ( ph -> ph ) }, { z | ( A. t t = t -> A. t t = t ) } and countless others are all universal classes whose equality one cannot prove without ax-ext 2445. See also bj-issetw 33734. A version with a dv condition between x and y and not requiring ax-13 1968 is proved as bj-vexwv 33731, while the degenerate instance is a simple consequence of abid 2454. (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.) Use bj-vexwv 33731 instead when sufficient. (New usage is discouraged.)
|- ph   =>    |- y e. { x | ph }
Theorem	bj-vexwvt 33730*	Closed form of bj-vexwv 33731 and version of bj-vexwt 33728 with a dv condition, which does not require ax-13 1968. (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
|- ( A. x ph -> y e. { x | ph } )
Theorem	bj-vexwv 33731*	Version of bj-vexw 33729 with a dv condition, which does not require ax-13 1968. The degenerate instance of bj-vexw 33729 is a simple consequence of abid 2454. (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
|- ph   =>    |- y e. { x | ph }
Theorem	bj-denotes 33732*	This would be the justification for the definition of the unary predicate "E!" by |- ( E! A <-> E. x x = A ) which could be interpreted as " A exists" or " A denotes". It is interesting that this justification can be proved without ax-ext 2445 nor df-cleq 2459 (but of course using df-clab 2453 and df-clel 2462). Once extensionality is postulated, then isset 3117 will prove that "existing" (as a set) is equivalent to being a member of a class. Note that there is no dv condition on x , y but the theorem does not depend on ax-13 1968. Actually, the proof depends only on ax-1--7 and sp 1808. The symbol "E!" was chosen to be reminiscent of the analogous predicate in (inclusive or non-inclusive) free logic, which deals with the possibility of non-existent objects. This analogy should not be taken too far, since here there are no equality axioms for classes: they are derived from ax-ext 2445 (e.g. eqid 2467). In particular, one cannot even prove |- E. x x = A => |- A = A. With ax-ext 2445, the present theorem is obvious from cbvexv 1997 and eqeq1 2471 (in free logic, the same proof holds since one has equality axioms for terms). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
|- ( E. x x = A <-> E. y y = A )
Theorem	bj-issetwt 33733*	Closed form of bj-issetw 33734. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
|- ( A. x ph -> ( A e. { x | ph } <-> E. y y = A ) )
Theorem	bj-issetw 33734*	The closest one can get to isset 3117 without using ax-ext 2445. See also bj-vexw 33729. Note that the only dv condition is between y and A. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
|- ph   =>    |- ( A e. { x | ph } <-> E. y y = A )
Theorem	bj-elissetv 33735*	Version of bj-elisset 33736 with a dv condition on x , V. This proof uses only df-ex 1597, ax-gen 1601, ax-4 1612 and df-clel 2462 on top of propositional calculus. Prefer its use over bj-elisset 33736 when sufficient. (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
|- ( A e. V -> E. x x = A )
Theorem	bj-elisset 33736*	Remove from elisset 3124 dependency on ax-ext 2445 (and on df-cleq 2459 and df-v 3115). This proof uses only df-clab 2453 and df-clel 2462 on top of first-order logic. It only uses ax-12 1803 among the auxiliary logical axioms. Use bj-elissetv 33735 instead when sufficient (in particular when V is substituted for _V). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
|- ( A e. V -> E. x x = A )
Theorem	bj-issetiv 33737*	Version of bj-isseti 33738 with a dv condition on x , V. This proof uses only df-ex 1597, ax-gen 1601, ax-4 1612 and df-clel 2462 on top of propositional calculus. Prefer its use over bj-isseti 33738 when sufficient (in particular when V is substituted for _V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
|- A e. V   =>    |- E. x x = A
Theorem	bj-isseti 33738*	Remove from isseti 3119 dependency on ax-ext 2445 (and on df-cleq 2459 and df-v 3115). This proof uses only df-clab 2453 and df-clel 2462 on top of first-order logic. It only uses ax-12 1803 among the auxiliary logical axioms. The hypothesis uses V instead of _V for extra generality. This is indeed more general as long as elex 3122 is not available. Use bj-issetiv 33737 instead when sufficient (in particular when V is substituted for _V). (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
|- A e. V   =>    |- E. x x = A
Theorem	bj-ralvw 33739	A weak version of ralv 3127 not using ax-ext 2445 (nor df-cleq 2459, df-clel 2462, df-v 3115), but using ax-13 1968. For the sake of illustration, the next theorem bj-rexvwv 33740, a weak version of rexv 3128, has a dv condition and avoids dependency on ax-13 1968, while the analogues for reuv 3129 and rmov 3130 are not proved. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ps   =>    |- ( A. x e. { y | ps } ph <-> A. x ph )
Theorem	bj-rexvwv 33740*	A weak version of rexv 3128 not using ax-ext 2445 (nor df-cleq 2459, df-clel 2462, df-v 3115) with an additional dv condition to avoid dependency on ax-13 1968 as well. See bj-ralvw 33739. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ps   =>    |- ( E. x e. { y | ps } ph <-> E. x ph )
Theorem	bj-rababwv 33741*	A weak version of rabab 3131 not using df-clel 2462 nor df-v 3115 (but requiring ax-ext 2445). A version without dv condition is provable by replacing bj-vexwv 33731 with bj-vexw 33729 in the proof, hence requiring ax-13 1968. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ps   =>    |- { x e. { y | ps } | ph } = { x | ph }
Theorem	bj-ralcom4 33742*	Remove from ralcom4 3132 dependency on ax-ext 2445 and ax-13 1968 (and on df-or 370, df-an 371, df-tru 1382, df-sb 1712, df-clab 2453, df-cleq 2459, df-clel 2462, df-nfc 2617, df-v 3115). This proof uses only df-ral 2819 on top of first-order logic. (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
|- ( A. x e. A A. y ph <-> A. y A. x e. A ph )
Theorem	bj-rexcom4 33743*	Remove from rexcom4 3133 dependency on ax-ext 2445 and ax-13 1968 (and on df-or 370, df-tru 1382, df-sb 1712, df-clab 2453, df-cleq 2459, df-clel 2462, df-nfc 2617, df-v 3115). This proof uses only df-rex 2820 on top of first-order logic. (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
|- ( E. x e. A E. y ph <-> E. y E. x e. A ph )
Theorem	bj-rexcom4a 33744*	Remove from rexcom4a 3134 dependency on ax-ext 2445 and ax-13 1968 (and on df-or 370, df-sb 1712, df-clab 2453, df-cleq 2459, df-clel 2462, df-nfc 2617, df-v 3115). This proof uses only df-rex 2820 on top of first-order logic. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ( E. x E. y e. A ( ph /\ ps ) <-> E. y e. A ( ph /\ E. x ps ) )
Theorem	bj-rexcom4bv 33745*	Version of bj-rexcom4b 33746 with a dv condition on x , V, hence removing dependency on df-sb 1712 and df-clab 2453 (so that it depends on df-clel 2462 and df-rex 2820 only on top of first-order logic). Prefer its use over bj-rexcom4b 33746 when sufficient (in particular when V is substituted for _V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
|- B e. V   =>    |- ( E. x E. y e. A ( ph /\ x = B ) <-> E. y e. A ph )
Theorem	bj-rexcom4b 33746*	Remove from rexcom4b 3135 dependency on ax-ext 2445 and ax-13 1968 (and on df-or 370, df-cleq 2459, df-nfc 2617, df-v 3115). The hypothesis uses V instead of _V (see bj-isseti 33738 for the motivation). Use bj-rexcom4bv 33745 instead when sufficient (in particular when V is substituted for _V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- B e. V   =>    |- ( E. x E. y e. A ( ph /\ x = B ) <-> E. y e. A ph )
Theorem	bj-ceqsalt0 33747	The FOL content of ceqsalt 3136. Lemma for bj-ceqsalt 33749 and bj-ceqsaltv 33750. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
|- ( ( F/ x ps /\ A. x ( th -> ( ph <-> ps ) ) /\ E. x th ) -> ( A. x ( th -> ph ) <-> ps ) )
Theorem	bj-ceqsalt1 33748	The FOL content of ceqsalt 3136. Lemma for bj-ceqsalt 33749 and bj-ceqsaltv 33750. (TODO: consider removing if it does not add anything to bj-ceqsalt0 33747.) (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
|- ( th -> E. x ch )   =>    |- ( ( F/ x ps /\ A. x ( ch -> ( ph <-> ps ) ) /\ th ) -> ( A. x ( ch -> ph ) <-> ps ) )
Theorem	bj-ceqsalt 33749*	Remove from ceqsalt 3136 dependency on ax-ext 2445 (and on df-cleq 2459 and df-v 3115). Note: this is not doable with ceqsralt 3137 (or ceqsralv 3142), which uses eleq1 2539, but the same dependence removal is possible for ceqsalg 3138, ceqsal 3140, ceqsalv 3141, cgsexg 3146, cgsex2g 3147, cgsex4g 3148, ceqsex 3149, ceqsexv 3150, ceqsex2 3151, ceqsex2v 3152, ceqsex3v 3153, ceqsex4v 3154, ceqsex6v 3155, ceqsex8v 3156, gencbvex 3157 (after changing A = y to y = A), gencbvex2 3158, gencbval 3159, vtoclgft 3161 (it uses F/_, whose justification nfcjust 2616 is actually provable without ax-ext 2445, as bj-nfcjust 33724 shows) and several other vtocl* theorems (see for instance bj-vtoclg1f 33781). See also bj-ceqsaltv 33750. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) <-> ps ) )
Theorem	bj-ceqsaltv 33750*	Version of bj-ceqsalt 33749 with a dv condition on x , V, removing dependency on df-sb 1712 and df-clab 2453. Prefer its use over bj-ceqsalt 33749 when sufficient (in particular when V is substituted for _V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) <-> ps ) )
Theorem	bj-ceqsalg0 33751	The FOL content of ceqsalg 3138. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( ch -> ( ph <-> ps ) )   =>    |- ( E. x ch -> ( A. x ( ch -> ph ) <-> ps ) )
Theorem	bj-ceqsalg 33752*	Remove from ceqsalg 3138 dependency on ax-ext 2445 (and on df-cleq 2459 and df-v 3115). See also bj-ceqsalgv 33754. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( A. x ( x = A -> ph ) <-> ps ) )
Theorem	bj-ceqsalgALT 33753*	Alternate proof of bj-ceqsalg 33752. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ps   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( A. x ( x = A -> ph ) <-> ps ) )
Theorem	bj-ceqsalgv 33754*	Version of bj-ceqsalg 33752 with a dv condition on x , V, removing dependency on df-sb 1712 and df-clab 2453. Prefer its use over bj-ceqsalg 33752 when sufficient (in particular when V is substituted for _V). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( A. x ( x = A -> ph ) <-> ps ) )
Theorem	bj-ceqsalgvALT 33755*	Alternate proof of bj-ceqsalgv 33754. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ x ps   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A e. V -> ( A. x ( x = A -> ph ) <-> ps ) )
Theorem	bj-ceqsal 33756*	Remove from ceqsal 3140 dependency on ax-ext 2445 (and on df-cleq 2459, df-v 3115, df-clab 2453, df-sb 1712). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- A e. _V   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A. x ( x = A -> ph ) <-> ps )
Theorem	bj-ceqsalv 33757*	Remove from ceqsalv 3141 dependency on ax-ext 2445 (and on df-cleq 2459, df-v 3115, df-clab 2453, df-sb 1712). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- A e. _V   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A. x ( x = A -> ph ) <-> ps )
21.29.5.3  The class-form not-free predicate In this section, we prove the symmetry of the class-form not-free predicate.
Theorem	bj-nfcsym 33758	The class-form not-free predicate defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 4676 with additional axioms; see also nfcv 2629). This could be proved from aecom 2024 and nfcvb 4677 but the latter requires a domain with at least two objects (hence uses extra axioms). (Contributed by BJ, 30-Sep-2018.) Proof modification is discouraged to avoid use of eqcomd 2475 instead of bj-equcomd 33535; removing dependency on ax-ext 2445 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2648, eleq2d 2537 (using elequ2 1772), nfcvf 2654, dvelimc 2653, dvelimdc 2652, nfcvf2 2655. (Proof modification is discouraged.)
|- ( F/_ x y <-> F/_ y x )
21.29.5.4  Proposal for the definitions of class membership and class equality In this section, we show (bj-ax8 33759 and bj-ax9 33762) that the current forms of the definitions of class membership (df-clel 2462) and class equality (df-cleq 2459) are too powerful, and we propose alternate definitions (bj-df-clel 33760 and bj-df-cleq 33763) which also have the advantage of making it clear that these definitions are conservative.
Theorem	bj-ax8 33759	Proof of ax-8 1769 from df-clel 2462 (and FOL). This shows that df-clel 2462 is "too powerful". A possible definition is given by bj-df-clel 33760. (Contributed by BJ, 27-Jun-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( x e. z -> y e. z ) )
Theorem	bj-df-clel 33760*	Candidate definition for df-clel 2462 (the need for it is exposed in bj-ax8 33759). The similarity of the hypothesis and the conclusion makes it clear that this definition merely extends to class variables something that is true for setvar variables, hence is conservative. This definition should be directly referenced only by bj-dfclel 33761, which should be used instead. The proof is irrelevant since this is a proposal for an axiom. Note: the current definition df-clel 2462 already mentions cleljust 2082 as a justification; here, we merely propose to put it as a hypothesis to make things clearer. (Contributed by BJ, 27-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( y e. z <-> E. x ( x = y /\ x e. z ) )   =>    |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
Theorem	bj-dfclel 33761*	Characterization of the elements of a class. (Contributed by BJ, 27-Jun-2019.) (Proof modification is discouraged.)
|- ( A e. B <-> E. x ( x = A /\ x e. B ) )
Theorem	bj-ax9 33762*	Proof of ax-9 1771 from ax-ext 2445 and df-cleq 2459 (and FOL). This shows that df-cleq 2459 is "too powerful". A possible definition is given by bj-df-cleq 33763. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( z e. x -> z e. y ) )
Theorem	bj-df-cleq 33763*	Candidate definition for df-cleq 2459 (the need for it is exposed in bj-ax9 33762). The similarity of the hypothesis and the conclusion makes it clear that this definition merely extends to class variables something that is true for setvar variables, hence is conservative. This definition should be directly referenced only by bj-dfcleq 33764, which should be used instead. The proof is irrelevant since this is a proposal for an axiom. Another definition, which would give finer control, is actually the pair of definitions where each has one implication of the present biconditional as hypothesis and conclusion. They assert that extensionality (respectively, the left-substitution axiom for the membership predicate) extends from setvars to classes. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( y = z <-> A. x ( x e. y <-> x e. z ) )   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
Theorem	bj-dfcleq 33764*	Proof of class extensionality from the axiom of set extensionality (ax-ext 2445) and the definition of class equality (bj-df-cleq 33763). (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( A = B <-> A. x ( x e. A <-> x e. B ) )
21.29.5.5  Lemmas for class substitution Some useful theorems for dealing with substitutions: sbbi 2116, sbcbig 3378, sbcel1g 3829, sbcel2 3831, sbcel12 3823, sbceqg 3825, csbvarg 3848.
Theorem	bj-sbeqALT 33765*	Substitution in an equality (use the more genereal version bj-sbeq 33766 instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
|- ( [ y / x ] A = B <-> [_ y / x ]_ A = [_ y / x ]_ B )
Theorem	bj-sbeq 33766	Distribute proper substitution through an equality relation. (See sbceqg 3825). (Contributed by BJ, 6-Oct-2018.)
|- ( [ y / x ] A = B <-> [_ y / x ]_ A = [_ y / x ]_ B )
Theorem	bj-sbceqgALT 33767	Distribute proper substitution through an equality relation. Alternate proof of sbceqg 3825. (Contributed by BJ, 6-Oct-2018.) Proof modification is discouraged to avoid using sbceqg 3825, but "minimize */except sbceqg" is ok. (Proof modification is discouraged.)
|- ( A e. V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) )
Theorem	bj-csbsnlem 33768*	Lemma for bj-csbsn 33769 (in this lemma, x cannot occur in A). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
|- [_ A / x ]_ { x } = { A }
Theorem	bj-csbsn 33769	Substitution in a singleton. (Contributed by BJ, 6-Oct-2018.)
|- [_ A / x ]_ { x } = { A }
Theorem	bj-sbel1 33770*	Version of sbcel1g 3829 when substituting a set. (Note: one could have a corresponding version of sbcel12 3823 when substituting a set, but the point here is that the antecedent of sbcel1g 3829 is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018.)
|- ( [ y / x ] A e. B <-> [_ y / x ]_ A e. B )
Theorem	bj-abtru 33771	The class of sets verifying a tautology is the universal class. (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
|- ( A. x ph -> { x | ph } = _V )
Theorem	bj-abfal 33772	The class of sets verifying a falsity is the empty set (closed form of abf 3819). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
|- ( A. x -. ph -> { x | ph } = (/) )
Theorem	bj-abf 33773	Shorter proof of abf 3819 (which should be kept as abfALT). (Contributed by BJ, 24-Jul-2019.)
|- -. ph   =>    |- { x | ph } = (/)
Theorem	bj-csbprc 33774	More direct proof of csbprc 3821 (fewer essential steps). (Contributed by BJ, 24-Jul-2019.)
|- ( -. A e. _V -> [_ A / x ]_ B = (/) )
21.29.5.6  Removing some dv conditions
Theorem	bj-exlimmpi 33775	Lemma for bj-vtoclg1f1 33780 (an instance of this lemma is a version of bj-vtoclg1f1 33780 where x and y are identified). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( ch -> ( ph -> ps ) )   &    |- ph   =>    |- ( E. x ch -> ps )
Theorem	bj-exlimmpbi 33776	Lemma for theorems of the vtoclg 3171 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( ch -> ( ph <-> ps ) )   &    |- ph   =>    |- ( E. x ch -> ps )
Theorem	bj-exlimmpbir 33777	Lemma for theorems of the vtoclg 3171 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
|- F/ x ph   &    |- ( ch -> ( ph <-> ps ) )   &    |- ps   =>    |- ( E. x ch -> ph )
Theorem	bj-vtoclf 33778*	Remove dependency on ax-ext 2445, df-clab 2453 and df-cleq 2459 (and df-sb 1712 and df-v 3115) from vtoclf 3164. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- A e. V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	bj-vtocl 33779*	Remove dependency on ax-ext 2445, df-clab 2453 and df-cleq 2459 (and df-sb 1712 and df-v 3115) from vtocl 3165. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- A e. V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	bj-vtoclg1f1 33780*	The FOL content of vtoclg1f 3170 (hence not using ax-ext 2445, df-cleq 2459, df-nfc 2617, df-v 3115). Note the weakened "major" hypothesis and the dv condition between x and A (needed since the class-form non-free predicate is not available without ax-ext 2445; as a byproduct, this dispenses with ax-11 1791 and ax-13 1968). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = A -> ( ph -> ps ) )   &    |- ph   =>    |- ( E. y y = A -> ps )
Theorem	bj-vtoclg1f 33781*	Reprove vtoclg1f 3170 from bj-vtoclg1f1 33780. This removes dependency on ax-ext 2445, df-cleq 2459 and df-v 3115. Use bj-vtoclg1fv 33782 instead when sufficient (in particular when V is substituted for _V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = A -> ( ph -> ps ) )   &    |- ph   =>    |- ( A e. V -> ps )
Theorem	bj-vtoclg1fv 33782*	Version of bj-vtoclg1f 33781 with a dv condition on x , V. This removes dependency on df-sb 1712 and df-clab 2453. Prefer its use over bj-vtoclg1f 33781 when sufficient (in particular when V is substituted for _V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = A -> ( ph -> ps ) )   &    |- ph   =>    |- ( A e. V -> ps )
Theorem	bj-rabbida2 33783	Version of rabbidva2 3103 with dv condition replaced by non-freeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
|- F/ x ph   &    |- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ch } )
Theorem	bj-rabbida 33784	Version of rabbidva 3104 with dv condition replaced by non-freeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> { x e. A | ps } = { x e. A | ch } )
Theorem	bj-rabbid 33785	Version of rabbidv 3105 with dv condition replaced by non-freeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { x e. A | ps } = { x e. A | ch } )
Theorem	bj-rabeqd 33786	Deduction form of rabeq 3107. Note that contrary to rabeq 3107 it has no dv condition. (Contributed by BJ, 27-Apr-2019.)
|- F/ x ph   &    |- ( ph -> A = B )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ps } )
Theorem	bj-rabeqbid 33787	Version of rabeqbidv 3108 with two dv conditions removed and the third replaced by a non-freeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
|- F/ x ph   &    |- ( ph -> A = B )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ch } )
Theorem	bj-rabeqbida 33788	Version of rabeqbidva 3109 with two dv conditions removed and the third replaced by a non-freeness hypothesis. (Contributed by BJ, 27-Apr-2019.)
|- F/ x ph   &    |- ( ph -> A = B )   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> { x e. A | ps } = { x e. B | ch } )
Theorem	bj-seex 33789*	Version of seex 4842 with a dv condition replaced by a non-freeness hypothesis (for the sake of illustration). (Contributed by BJ, 27-Apr-2019.)
|- F/_ x B   =>    |- ( ( R Se A /\ B e. A ) -> { x e. A | x R B } e. _V )
Theorem	bj-nfcf 33790*	Version of df-nfc 2617 with a dv condition replaced with a non-freeness hypothesis. (Contributed by BJ, 2-May-2019.)
|- F/_ y A   =>    |- ( F/_ x A <-> A. y F/ x y e. A )
Theorem	bj-axsep2 33791*	Remove dependency on ax-13 1968, ax-ext 2445, df-cleq 2459 and df-clel 2462 from axsep2 4569 while shortening its proof. Remark: the comment in zfauscl 4570 is misleading: the essential use of ax-ext 2445 is the one via eleq2 2540 and not the one via vtocl 3165, since the latter can be proved without ax-ext 2445 (see bj-vtocl 33779). (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- E. y A. x ( x e. y <-> ( x e. z /\ ph ) )
21.29.5.7  Class abstractions A few additional theorems on class abstractions and restricted class abstractions.
Theorem	bj-unrab 33792*	Generalization of unrab 3769. Equality need not hold. (Contributed by BJ, 21-Apr-2019.)
|- ( { x e. A | ph } u. { x e. B | ps } ) C_ { x e. ( A u. B ) | ( ph \/ ps ) }
Theorem	bj-inrab 33793	Generalization of inrab 3770. (Contributed by BJ, 21-Apr-2019.)
|- ( { x e. A | ph } i^i { x e. B | ps } ) = { x e. ( A i^i B ) | ( ph /\ ps ) }
Theorem	bj-inrab2 33794	Shorter proof of inrab 3770. (Contributed by BJ, 21-Apr-2019.) (Proof modification is discouraged.)
|- ( { x e. A | ph } i^i { x e. A | ps } ) = { x e. A | ( ph /\ ps ) }
Theorem	bj-rabtr 33795*	Restricted class abstraction with true formula. (Contributed by BJ, 22-Apr-2019.)
|- { x e. A | T. } = A
Theorem	bj-rabtrALT 33796*	Alternate proof of bj-rabtr 33795. (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- { x e. A | T. } = A
Theorem	bj-rabtrAUTO 33797*	Proof of bj-rabtr 33795 found automatically by "improve all /depth 3 /3" followed by "minimize *" (which at some point used dummylink 1). (Contributed by BJ, 22-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- { x e. A | T. } = A
21.29.5.8  Russell's paradox A few results around Russell's paradox. For clarity, we prove separately its FOL part (bj-ru0 33798) and then two versions (bj-ru1 33799 and bj-ru 33800). Special attention is put on minimizing axiom depencencies.
Theorem	bj-ru0 33798*	The FOL part of Russell's paradox ru 3330 (see also bj-ru1 33799, bj-ru 33800). Use of elequ1 1770, bj-elequ12 33538, bj-spvv 33583 (instead of eleq1 2539, eleq12d 2549, spv 1980 as in ru 3330) permits to remove dependency on ax-11 1791, ax-13 1968, ax-ext 2445, df-sb 1712, df-clab 2453, df-cleq 2459, df-clel 2462. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- -. A. x ( x e. y <-> -. x e. x )
Theorem	bj-ru1 33799*	A version of Russell's paradox ru 3330 (see also bj-ru 33800). Note the more economical use of bj-abeq2 33657 instead of abeq2 2591 to avoid dependency on ax-13 1968. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- -. E. y y = { x | -. x e. x }
Theorem	bj-ru 33800	Remove dependency on ax-13 1968 (and df-v 3115) from Russell's paradox ru 3330 expressed with primitive symbols and with a class variable V. Note the more economical use of bj-elissetv 33735 instead of isset 3117 to avoid use of df-v 3115. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- -. { x | -. x e. x } e. V