P. 329 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32801-32900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-dtrucor2v 32801*	Version of dtrucor2 4901 with a dv condition, which does not require ax-13 2246 (nor ax-4 1737, ax-5 1839, ax-7 1935, ax-12 2047). (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.)
|- ( x = y -> x =/= y )   =>    |- ( ph /\ -. ph )
Theorem	bj-dvdemo1 32802*	Remove dependency on ax-13 2246 from dvdemo1 4902 (this removal is noteworthy since dvdemo1 4902 and dvdemo2 4903 illustrate the phenomenon of bundling). (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.)
|- E. x ( x = y -> z e. x )
Theorem	bj-dvdemo2 32803*	Remove dependency on ax-13 2246 from dvdemo2 4903 (this removal is noteworthy since dvdemo1 4902 and dvdemo2 4903 illustrate the phenomenon of bundling). (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.)
|- E. x ( x = y -> z e. x )
20.14.4.12  Strengthenings of theorems of the main part Typically, these are biconditional versions of theorems in the main part which are formulated as implications. They could be added after said implication, or sometimes replace it (by "inlining" it). This could also be done for hba1 2151, hbe1 2021, hbn1 2020, modal-5 2032.
Theorem	bj-sb3b 32804	Simplified definition of substitution when variables are distinct. This is to sb3 2355 what sb4b 2358 is to sb4 2356. Actually, one may keep only bj-sb3b 32804 and sb4b 2358 in the database, renaming them sb3 and sb4. (Contributed by BJ, 6-Oct-2018.)
|- ( -. A. x x = y -> ( [ y / x ] ph <-> E. x ( x = y /\ ph ) ) )
20.14.4.13  Distinct var metavariables The closed formula A. x A. y x = y approximately means that the var metavariables x and y represent the same variable vi. In a domain with at most one object, however, this formula is always true, hence the "approximately" in the previous sentence.
Theorem	bj-hbaeb2 32805	Biconditional version of a form of hbae 2315 with commuted quantifiers, not requiring ax-11 2034. (Contributed by BJ, 12-Dec-2019.) (Proof modification is discouraged.)
|- ( A. x x = y <-> A. x A. z x = y )
Theorem	bj-hbaeb 32806	Biconditional version of hbae 2315. (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.)
|- ( A. x x = y <-> A. z A. x x = y )
Theorem	bj-hbnaeb 32807	Biconditional version of hbnae 2317 (to replace it?). (Contributed by BJ, 6-Oct-2018.)
|- ( -. A. x x = y <-> A. z -. A. x x = y )
Theorem	bj-dvv 32808	A special instance of bj-hbaeb2 32805. A lemma for distinct var metavariables. Note that the right-hand side is a closed formula (a sentence). (Contributed by BJ, 6-Oct-2018.)
|- ( A. x x = y <-> A. x A. y x = y )
20.14.4.14  Around ~ equsal As a rule of thumb, if a theorem of the form |- ( ph <-> ps ) => |- ( ch <-> th ) is in the database, and the "more precise" theorems |- ( ph -> ps ) => |- ( ch -> th ) and |- ( ps -> ph ) => |- ( th -> ch ) also hold (see bj-bisym 32575), then they should be added to the database. The present case is similar. Similar additions can be done regarding equsex 2292 (and equsalh 2294 and equsexh 2295). Even if only one of these two theorems holds, it should be added to the database.
Theorem	bj-equsal1t 32809	Duplication of wl-equsal1t 33327, with shorter proof. If one imposes a DV condition on x,y , then one can use bj-alequexv 32655 and reduce axiom dependencies, and similarly for the following theorems. Note: wl-equsalcom 33328 is also interesting. (Contributed by BJ, 6-Oct-2018.)
|- ( F/ x ph -> ( A. x ( x = y -> ph ) <-> ph ) )
Theorem	bj-equsal1ti 32810	Inference associated with bj-equsal1t 32809. (Contributed by BJ, 30-Sep-2018.)
|- F/ x ph   =>    |- ( A. x ( x = y -> ph ) <-> ph )
Theorem	bj-equsal1 32811	One direction of equsal 2291. (Contributed by BJ, 30-Sep-2018.)
|- F/ x ps   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( A. x ( x = y -> ph ) -> ps )
Theorem	bj-equsal2 32812	One direction of equsal 2291. (Contributed by BJ, 30-Sep-2018.)
|- F/ x ph   &    |- ( x = y -> ( ph -> ps ) )   =>    |- ( ph -> A. x ( x = y -> ps ) )
Theorem	bj-equsal 32813	Shorter proof of equsal 2291. (Contributed by BJ, 30-Sep-2018.) Proof modification is discouraged to avoid using equsal 2291, but "min */exc equsal" is ok. (Proof modification is discouraged.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ( x = y -> ph ) <-> ps )
20.14.4.15  Some Principia Mathematica proofs References are made to the second edition (1927, reprinted 1963) of Principia Mathematica, Vol. 1. Theorems are referred to in the form "PM*xx.xx".
Theorem	stdpc5t 32814	Closed form of stdpc5 2076. (Possible to place it before 19.21t 2073 and use it to prove 19.21t 2073). (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
|- ( F/ x ph -> ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) ) )
Theorem	bj-stdpc5 32815	More direct proof of stdpc5 2076. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
|- F/ x ph   =>    |- ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) )
Theorem	2stdpc5 32816	A double stdpc5 2076 (one direction of PM*11.3). See also 2stdpc4 2354 and 19.21vv 38575. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
|- F/ x ph   &    |- F/ y ph   =>    |- ( A. x A. y ( ph -> ps ) -> ( ph -> A. x A. y ps ) )
Theorem	bj-19.21t 32817	Proof of 19.21t 2073 from stdpc5t 32814. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
|- ( F/ x ph -> ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) ) )
Theorem	exlimii 32818	Inference associated with exlimi 2086. 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 32819	Proof of ax-11 2034 similar to PM's proof of alcom 2037 (PM*11.2). For a proof closer to PM's proof, see ax11-pm2 32823. Axiom ax-11 2034 is used in the proof only through nfa2 2040. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
|- ( A. x A. y ph -> A. y A. x ph )
Theorem	ax6er 32820	Commuted form of ax6e 2250. (Could be placed right after ax6e 2250). (Contributed by BJ, 15-Sep-2018.)
|- E. x y = x
Theorem	exlimiieq1 32821	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 32822	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 32823*	Proof of ax-11 2034 from the standard axioms of predicate calculus, similar to PM's proof of alcom 2037 (PM*11.2). This proof requires that x and y be distinct. Axiom ax-11 2034 is used in the proof only through nfal 2153, nfsb 2440, sbal 2462, sb8 2424. See also ax11-pm 32819. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
|- ( A. x A. y ph -> A. y A. x ph )
20.14.4.16  Alternate definition of substitution
Theorem	bj-sbsb 32824	Biconditional showing two possible (dual) definitions of substitution df-sb 1881 not using dummy variables. (Contributed by BJ, 19-Mar-2021.)
|- ( ( ( x = y -> ph ) /\ E. x ( x = y /\ ph ) ) <-> ( A. x ( x = y -> ph ) \/ ( x = y /\ ph ) ) )
Theorem	bj-dfsb2 32825	Alternate (dual) definition of substitution df-sb 1881 not using dummy variables. (Contributed by BJ, 19-Mar-2021.)
|- ( [ y / x ] ph <-> ( A. x ( x = y -> ph ) \/ ( x = y /\ ph ) ) )
20.14.4.17  Lemmas for substitution
Theorem	bj-sbf3 32826	Substitution has no effect on a bound variabe (existential quantifier case); see sbf2 2382. (Contributed by BJ, 2-May-2019.)
|- ( [ y / x ] E. x ph <-> E. x ph )
Theorem	bj-sbf4 32827	Substitution has no effect on a bound variabe (non-freeness case); see sbf2 2382. (Contributed by BJ, 2-May-2019.)
|- ( [ y / x ] F/ x ph <-> F/ x ph )
Theorem	bj-sbnf 32828*	Move non-free predicate in and out of substitution; see sbal 2462 and sbex 2463. (Contributed by BJ, 2-May-2019.)
|- ( [ z / y ] F/ x ph <-> F/ x [ z / y ] ph )
20.14.4.18  Existential uniqueness
Theorem	bj-eu3f 32829*	Version of eu3v 2498 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 2498. (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 32830*	Existential uniqueness implies "at most one." Used to be in the main part and deprecated in favor of eumo 2499 and mo2 2479. (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 ) )
20.14.4.19  First-logic: miscellaneous Miscellaneous theorems of first-order logic.
Theorem	bj-sbidmOLD 32831	Obsolete proof of sbidm 2414 temporarily kept here to check it gives no additional insight. (Contributed by NM, 8-Mar-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( [ y / x ] [ y / x ] ph <-> [ y / x ] ph )
Theorem	bj-mo3OLD 32832*	Obsolete proof of mo3 2507 temporarily kept here to check it gives no additional insight. (Contributed by NM, 8-Mar-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ y ph   =>    |- ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
Theorem	bj-syl66ib 32833	A mixed syllogism inference derived from syl6ib 241. In addition to bj-dvelimdv1 32835, it can also shorten alexsubALTlem4 21854 (4821>4812), supsrlem 9932 (2868>2863). (Contributed by BJ, 20-Oct-2021.)
|- ( ph -> ( ps -> th ) )   &    |- ( th -> ta )   &    |- ( ta <-> ch )   =>    |- ( ph -> ( ps -> ch ) )
Theorem	bj-dvelimdv 32834*	Deduction form of dvelim 2337 with DV conditions. Uncurried (imported) form of bj-dvelimdv 32834. Typically, z is a fresh variable used for the implicit substitution hypothesis that results in ch (namely, ps can be thought as ps ( x , y ) and ch as ps ( x , z )). So the theorem says that if x is effectively free in ps ( x , z ), then if x and y are not the same variable, then x is also effectively free in ps ( x , y ), in a context ph. One can weakend the implicit substitution hypothesis by adding the antecedent ph but this typically does not make the theorem much more useful. Similarly, one could use non-freeness hypotheses instead of DV conditions but since this result is typically used when z is a dummy variable, this would not be of much benefit. One could also remove DV(z,x) since in the proof nfv 1843 can be replaced with nfal 2153 followed by nfn 1784. Remark: nfald 2165 uses ax-11 2034; it might be possible to inline and use ax11w 2007 instead, but there is still a use via 19.12 2164 anyway. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
|- F/ x ph   &    |- ( ph -> F/ x ch )   &    |- ( z = y -> ( ch <-> ps ) )   =>    |- ( ( ph /\ -. A. x x = y ) -> F/ x ps )
Theorem	bj-dvelimdv1 32835*	Curried (exported) form of bj-dvelimdv 32834. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
|- F/ x ph   &    |- ( ph -> F/ x ch )   &    |- ( z = y -> ( ch <-> ps ) )   =>    |- ( ph -> ( -. A. x x = y -> F/ x ps ) )
Theorem	bj-dvelimv 32836*	A version of dvelim 2337 using the "non-free" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
|- F/ x ps   &    |- ( z = y -> ( ps <-> ph ) )   =>    |- ( -. A. x x = y -> F/ x ph )
Theorem	bj-nfeel2 32837*	Non-freeness in an equality. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
|- ( -. A. x x = y -> F/ x y e. z )
Theorem	bj-axc14nf 32838	Proof of a version of axc14 2372 using the "non-free" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
|- ( -. A. z z = x -> ( -. A. z z = y -> F/ z x e. y ) )
Theorem	bj-axc14 32839	Alternate proof of axc14 2372 (even when inlining the above results, this gives a shorter proof). (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
|- ( -. A. z z = x -> ( -. A. z z = y -> ( x e. y -> A. z x e. y ) ) )
20.14.5  Set theory
20.14.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 2602, df-clab 2609, df-cleq 2615, df-clel 2618 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 2602, df-clab 2609, df-cleq 2615, df-clel 2618 }) 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 32840 and the following theorems of this section, which are special instances of df-clab 2609, dfcleq 2616 (proved from {FOL, ax-ext 2602, df-cleq 2615 }), and df-clel 2618. 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 32841, eliminable2b 32842 and eliminable3a 32844, 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 1482, 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 2609 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 2609, ax-ext 2602 and df-cleq 2615 are sufficient (over FOL) to eliminate class terms. To prove that { df-clab 2609, df-cleq 2615, df-clel 2618 } provides a definitional extension of {FOL, ax-ext 2602 }, 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 2609, df-cleq 2615, df-clel 2618 }. 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 2602 }. 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 2609, df-cleq 2615, df-clel 2618 }. It involves a careful case study on the structure of the proof tree.
Theorem	eliminable1 32840	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 32841*	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 32842*	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 32843*	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 32844*	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 32845*	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 32846*	Every class can be written as (is equal to) a class abstraction. cvjust 2617 is a special instance of it, but the present proof does not require ax-13 2246, contrary to cvjust 2617. This theorem requires ax-ext 2602, df-clab 2609, df-cleq 2615, df-clel 2618, 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 1482, cab 2608 and statements corresponding to defined class constructors. UPDATE: This theorem is (almost) abid2 2745 and bj-abid2 32782, though the present proof is shorter than a proof from bj-abid2 32782 and eqcomi 2631 (and is shorter than the proof of either); plus, it is of the same form as cvjust 2617 and such a basic statement deserves to be present in both forms. Note that bj-termab 32846 shortens the proof of abid2 2745, and shortens five proofs by a total of 72 bytes. Move it to Main as "abid1" proved from abbi2i 2738? Note also that this is the form in Quine, more than abid2 2745. (Contributed by BJ, 21-Oct-2019.) (Proof modification is discouraged.)
|- A = { x | x e. A }
20.14.5.2  Classes without extensionality A few results about classes can be proved without using ax-ext 2602. One could move all theorems from cab 2608 to df-clel 2618 (except for dfcleq 2616 and cvjust 2617) 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 2615. Note that without ax-ext 2602, the $a-statements df-clab 2609, df-cleq 2615, and df-clel 2618 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 2602, 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 1990, wel 1991, ax-8 1992, ax-9 1999). Remark: the weakening of eleq1 2689 / eleq2 2690 to eleq1w 2684 / eleq2w 2685 can also be done with eleq1i 2692, eqeltri 2697, eqeltrri 2698, eleq1a 2696, eleq1d 2686, eqeltrd 2701, eqeltrrd 2702, eqneltrd 2720, eqneltrrd 2721, nelneq 2725.
Theorem	bj-cleljustab 32847*	An instance of df-clel 2618 where the LHS (the definiendum) has the form "setvar e. class abstraction". The straightforward yet important fact that this statement can be proved from FOL= and df-clab 2609 (hence without df-clel 2618 or df-cleq 2615) was stressed by Mario Carneiro. The instance of df-clel 2618 where the LHS has the form "setvar e. setvar" is proved as cleljust 1998, from FOL= and ax-8 1992. Note: when df-ssb 32620 is the official definition for substitution, one can use bj-ssbequ instead of sbequ 2376 to prove bj-cleljustab 32847 from Tarski's FOL= with df-clab 2609. (Contributed by BJ, 8-Nov-2021.) (Proof modification is discouraged.)
|- ( x e. { y | ph } <-> E. z ( z = x /\ z e. { y | ph } ) )
Theorem	bj-clelsb3 32848*	Remove dependency on ax-ext 2602 (and df-cleq 2615) from clelsb3 2729. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( [ x / y ] y e. A <-> x e. A )
Theorem	bj-hblem 32849*	Remove dependency on ax-ext 2602 (and df-cleq 2615) from hblem 2731. (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 32850*	Remove dependency on ax-ext 2602 (and df-cleq 2615 and ax-13 2246) from nfcjust 2752. (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 32851*	Remove dependency on ax-ext 2602 (and df-cleq 2615) from nfcrii 2757. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- F/_ x A   =>    |- ( y e. A -> A. x y e. A )
Theorem	bj-nfcri 32852*	Remove dependency on ax-ext 2602 (and df-cleq 2615) from nfcri 2758. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- F/_ x A   =>    |- F/ x y e. A
Theorem	bj-nfnfc 32853	Remove dependency on ax-ext 2602 (and df-cleq 2615) from nfnfc 2774. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
|- F/_ x A   =>    |- F/ x F/_ y A
Theorem	bj-vexwt 32854	Closed form of bj-vexw 32855. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) Use bj-vexwvt 32856 instead when sufficient. (New usage is discouraged.)
|- ( A. x ph -> y e. { x | ph } )
Theorem	bj-vexw 32855	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 3203, without using ax-ext 2602. Note that this theorem has no dv condition and does not use df-clel 2618 nor df-cleq 2615 either: only first-order logic and df-clab 2609. Without ax-ext 2602, one cannot define "the" universal class, since one could not prove for instance the justification theorem { x | T. } = { y | T. } (see vjust 3201). Indeed, in order to prove any equality of classes, one needs df-cleq 2615, which has ax-ext 2602 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 2602. See also bj-issetw 32860. A version with a dv condition between x and y and not requiring ax-13 2246 is proved as bj-vexwv 32857, while the degenerate instance is a simple consequence of abid 2610. (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.) Use bj-vexwv 32857 instead when sufficient. (New usage is discouraged.)
|- ph   =>    |- y e. { x | ph }
Theorem	bj-vexwvt 32856*	Closed form of bj-vexwv 32857 and version of bj-vexwt 32854 with a dv condition, which does not require ax-13 2246. (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
|- ( A. x ph -> y e. { x | ph } )
Theorem	bj-vexwv 32857*	Version of bj-vexw 32855 with a dv condition, which does not require ax-13 2246. The degenerate instance of bj-vexw 32855 is a simple consequence of abid 2610 (which does not depend on ax-13 2246 either). (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
|- ph   =>    |- y e. { x | ph }
Theorem	bj-denotes 32858*	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 2602 nor df-cleq 2615 (but of course using df-clab 2609 and df-clel 2618). Once extensionality is postulated, then isset 3207 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 2246. Actually, the proof depends only on ax-1--7 and sp 2053. 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 2602 (e.g., eqid 2622). In particular, one cannot even prove |- E. x x = A => |- A = A. With ax-ext 2602, the present theorem is obvious from cbvexv 2275 and eqeq1 2626 (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 32859*	Closed form of bj-issetw 32860. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
|- ( A. x ph -> ( A e. { x | ph } <-> E. y y = A ) )
Theorem	bj-issetw 32860*	The closest one can get to isset 3207 without using ax-ext 2602. See also bj-vexw 32855. 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 32861*	Version of bj-elisset 32862 with a dv condition on x , V. This proof uses only df-ex 1705, ax-gen 1722, ax-4 1737 and df-clel 2618 on top of propositional calculus. Prefer its use over bj-elisset 32862 when sufficient. (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
|- ( A e. V -> E. x x = A )
Theorem	bj-elisset 32862*	Remove from elisset 3215 dependency on ax-ext 2602 (and on df-cleq 2615 and df-v 3202). This proof uses only df-clab 2609 and df-clel 2618 on top of first-order logic. It only requires ax-1--7 and sp 2053. Use bj-elissetv 32861 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 32863*	Version of bj-isseti 32864 with a dv condition on x , V. This proof uses only df-ex 1705, ax-gen 1722, ax-4 1737 and df-clel 2618 on top of propositional calculus. Prefer its use over bj-isseti 32864 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 32864*	Remove from isseti 3209 dependency on ax-ext 2602 (and on df-cleq 2615 and df-v 3202). This proof uses only df-clab 2609 and df-clel 2618 on top of first-order logic. It only uses ax-12 2047 among the auxiliary logical axioms. The hypothesis uses V instead of _V for extra generality. This is indeed more general as long as elex 3212 is not available. Use bj-issetiv 32863 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 32865	A weak version of ralv 3219 not using ax-ext 2602 (nor df-cleq 2615, df-clel 2618, df-v 3202), but using ax-13 2246. For the sake of illustration, the next theorem bj-rexvwv 32866, a weak version of rexv 3220, has a dv condition and avoids dependency on ax-13 2246, while the analogues for reuv 3221 and rmov 3222 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 32866*	A weak version of rexv 3220 not using ax-ext 2602 (nor df-cleq 2615, df-clel 2618, df-v 3202) with an additional dv condition to avoid dependency on ax-13 2246 as well. See bj-ralvw 32865. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ps   =>    |- ( E. x e. { y | ps } ph <-> E. x ph )
Theorem	bj-rababwv 32867*	A weak version of rabab 3223 not using df-clel 2618 nor df-v 3202 (but requiring ax-ext 2602). A version without dv condition is provable by replacing bj-vexwv 32857 with bj-vexw 32855 in the proof, hence requiring ax-13 2246. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
|- ps   =>    |- { x e. { y | ps } | ph } = { x | ph }
Theorem	bj-ralcom4 32868*	Remove from ralcom4 3224 dependency on ax-ext 2602 and ax-13 2246 (and on df-or 385, df-an 386, df-tru 1486, df-sb 1881, df-clab 2609, df-cleq 2615, df-clel 2618, df-nfc 2753, df-v 3202). This proof uses only df-ral 2917 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 32869*	Remove from rexcom4 3225 dependency on ax-ext 2602 and ax-13 2246 (and on df-or 385, df-tru 1486, df-sb 1881, df-clab 2609, df-cleq 2615, df-clel 2618, df-nfc 2753, df-v 3202). This proof uses only df-rex 2918 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 32870*	Remove from rexcom4a 3226 dependency on ax-ext 2602 and ax-13 2246 (and on df-or 385, df-sb 1881, df-clab 2609, df-cleq 2615, df-clel 2618, df-nfc 2753, df-v 3202). This proof uses only df-rex 2918 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 32871*	Version of bj-rexcom4b 32872 with a dv condition on x , V, hence removing dependency on df-sb 1881 and df-clab 2609 (so that it depends on df-clel 2618 and df-rex 2918 only on top of first-order logic). Prefer its use over bj-rexcom4b 32872 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 32872*	Remove from rexcom4b 3227 dependency on ax-ext 2602 and ax-13 2246 (and on df-or 385, df-cleq 2615, df-nfc 2753, df-v 3202). The hypothesis uses V instead of _V (see bj-isseti 32864 for the motivation). Use bj-rexcom4bv 32871 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 32873	The FOL content of ceqsalt 3228. Lemma for bj-ceqsalt 32875 and bj-ceqsaltv 32876. (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 32874	The FOL content of ceqsalt 3228. Lemma for bj-ceqsalt 32875 and bj-ceqsaltv 32876. (TODO: consider removing if it does not add anything to bj-ceqsalt0 32873.) (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 32875*	Remove from ceqsalt 3228 dependency on ax-ext 2602 (and on df-cleq 2615 and df-v 3202). Note: this is not doable with ceqsralt 3229 (or ceqsralv 3234), which uses eleq1 2689, but the same dependence removal is possible for ceqsalg 3230, ceqsal 3232, ceqsalv 3233, cgsexg 3238, cgsex2g 3239, cgsex4g 3240, ceqsex 3241, ceqsexv 3242, ceqsex2 3244, ceqsex2v 3245, ceqsex3v 3246, ceqsex4v 3247, ceqsex6v 3248, ceqsex8v 3249, gencbvex 3250 (after changing A = y to y = A), gencbvex2 3251, gencbval 3252, vtoclgft 3254 (it uses F/_, whose justification nfcjust 2752 is actually provable without ax-ext 2602, as bj-nfcjust 32850 shows) and several other vtocl* theorems (see for instance bj-vtoclg1f 32911). See also bj-ceqsaltv 32876. (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 32876*	Version of bj-ceqsalt 32875 with a dv condition on x , V, removing dependency on df-sb 1881 and df-clab 2609. Prefer its use over bj-ceqsalt 32875 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 32877	The FOL content of ceqsalg 3230. (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 32878*	Remove from ceqsalg 3230 dependency on ax-ext 2602 (and on df-cleq 2615 and df-v 3202). See also bj-ceqsalgv 32880. (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 32879*	Alternate proof of bj-ceqsalg 32878. (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 32880*	Version of bj-ceqsalg 32878 with a dv condition on x , V, removing dependency on df-sb 1881 and df-clab 2609. Prefer its use over bj-ceqsalg 32878 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 32881*	Alternate proof of bj-ceqsalgv 32880. (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 32882*	Remove from ceqsal 3232 dependency on ax-ext 2602 (and on df-cleq 2615, df-v 3202, df-clab 2609, df-sb 1881). (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 32883*	Remove from ceqsalv 3233 dependency on ax-ext 2602 (and on df-cleq 2615, df-v 3202, df-clab 2609, df-sb 1881). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
|- A e. _V   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( A. x ( x = A -> ph ) <-> ps )
Theorem	bj-spcimdv 32884*	Remove from spcimdv 3290 dependency on ax-9 1999, ax-10 2019, ax-11 2034, ax-13 2246, ax-ext 2602, df-cleq 2615 (and df-nfc 2753, df-v 3202, df-or 385, df-tru 1486, df-nf 1710). For an even more economical version, see bj-spcimdvv 32885. (Contributed by BJ, 30-Nov-2020.) (Proof modification is discouraged.)
|- ( ph -> A e. B )   &    |- ( ( ph /\ x = A ) -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x ps -> ch ) )
Theorem	bj-spcimdvv 32885*	Remove from spcimdv 3290 dependency on ax-7 1935, ax-8 1992, ax-10 2019, ax-11 2034, ax-12 2047 ax-13 2246, ax-ext 2602, df-cleq 2615, df-clab 2609 (and df-nfc 2753, df-v 3202, df-or 385, df-tru 1486, df-nf 1710) at the price of adding a DV condition on x , B (but in usages, x is typically a dummy, hence fresh, variable). For the version without this DV condition, see bj-spcimdv 32884. (Contributed by BJ, 3-Nov-2021.) (Proof modification is discouraged.)
|- ( ph -> A e. B )   &    |- ( ( ph /\ x = A ) -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x ps -> ch ) )
20.14.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 32886	The class-form not-free predicate defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 4897 with additional axioms; see also nfcv 2764). This could be proved from aecom 2311 and nfcvb 4898 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 2628 instead of equcomd 1946; removing dependency on ax-ext 2602 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2782, eleq2d 2687 (using elequ2 2004), nfcvf 2788, dvelimc 2787, dvelimdc 2786, nfcvf2 2789. (Proof modification is discouraged.)
|- ( F/_ x y <-> F/_ y x )
20.14.5.4  Proposal for the definitions of class membership and class equality In this section, we show (bj-ax8 32887 and bj-ax9 32890) that the current forms of the definitions of class membership (df-clel 2618) and class equality (df-cleq 2615) are too powerful, and we propose alternate definitions (bj-df-clel 32888 and bj-df-cleq 32893) which also have the advantage of making it clear that these definitions are conservative.
Theorem	bj-ax8 32887	Proof of ax-8 1992 from df-clel 2618 (and FOL). This shows that df-clel 2618 is "too powerful". A possible definition is given by bj-df-clel 32888. (Contributed by BJ, 27-Jun-2019.) Also a direct consequence of eleq1w 2684, which has essentially the same proof. (Proof modification is discouraged.)
|- ( x = y -> ( x e. z -> y e. z ) )
Theorem	bj-df-clel 32888*	Candidate definition for df-clel 2618 (the need for it is exposed in bj-ax8 32887). The similarity of the hypothesis and the conclusion, together with all possible dv conditions, 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 32889, which should be used instead. The proof is irrelevant since this is a proposal for an axiom. Note: the current definition df-clel 2618 already mentions cleljust 1998 as a justification; here, we merely propose to put it (more preciesly: its universal closure) as a hypothesis to make things more explicit. (Contributed by BJ, 27-Jun-2019.) (Proof modification is discouraged.)
|- A. u A. v ( u e. v <-> E. w ( w = u /\ w e. v ) )   =>    |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
Theorem	bj-dfclel 32889*	Characterization of the elements of a class. Note: cleljust 1998 could be relabeled "clelhyp". (Contributed by BJ, 27-Jun-2019.) (Proof modification is discouraged.)
|- ( A e. B <-> E. x ( x = A /\ x e. B ) )
Theorem	bj-ax9 32890*	Proof of ax-9 1999 from Tarski's FOL=, sp 2053, df-cleq 2615 and ax-ext 2602 (with two extra dv conditions on x , z and y , z). For a version without these dv conditions, see bj-ax9-2 32891. This shows that df-cleq 2615 is "too powerful". A possible definition is given by bj-df-cleq 32893. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( z e. x -> z e. y ) )
Theorem	bj-ax9-2 32891	Proof of ax-9 1999 from Tarski's FOL=, ax-8 1992 (specifically, ax8v1 1994 and ax8v2 1995) , df-cleq 2615 and ax-ext 2602. For a version not using ax-8 1992, see bj-ax9 32890. This shows that df-cleq 2615 is "too powerful". A possible definition is given by bj-df-cleq 32893. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( z e. x -> z e. y ) )
Theorem	bj-cleqhyp 32892*	The hypothesis of bj-df-cleq 32893. Note that the hypothesis of bj-df-cleq 32893 actually has an additional dv condition on x , y and therefore is provable by simply using ax-ext 2602 in place of axext3 2604 in the current proof. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( x = y <-> A. z ( z e. x <-> z e. y ) )
Theorem	bj-df-cleq 32893*	Candidate definition for df-cleq 2615 (the need for it is exposed in bj-ax9 32890). 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 32894, 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.)
|- A. u A. v ( u = v <-> A. w ( w e. u <-> w e. v ) )   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
Theorem	bj-dfcleq 32894*	Proof of class extensionality from the axiom of set extensionality (ax-ext 2602) and the definition of class equality (bj-df-cleq 32893). (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
|- ( A = B <-> A. x ( x e. A <-> x e. B ) )
20.14.5.5  Lemmas for class substitution Some useful theorems for dealing with substitutions: sbbi 2401, sbcbig 3480, sbcel1g 3987, sbcel2 3989, sbcel12 3983, sbceqg 3984, csbvarg 4003.
Theorem	bj-sbeqALT 32895*	Substitution in an equality (use the more genereal version bj-sbeq 32896 instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( [ y / x ] A = B <-> [_ y / x ]_ A = [_ y / x ]_ B )
Theorem	bj-sbeq 32896	Distribute proper substitution through an equality relation. (See sbceqg 3984). (Contributed by BJ, 6-Oct-2018.)
|- ( [ y / x ] A = B <-> [_ y / x ]_ A = [_ y / x ]_ B )
Theorem	bj-sbceqgALT 32897	Distribute proper substitution through an equality relation. Alternate proof of sbceqg 3984. (Contributed by BJ, 6-Oct-2018.) Proof modification is discouraged to avoid using sbceqg 3984, but "minimize */except sbceqg" is ok. (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A e. V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) )
Theorem	bj-csbsnlem 32898*	Lemma for bj-csbsn 32899 (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 32899	Substitution in a singleton. (Contributed by BJ, 6-Oct-2018.)
|- [_ A / x ]_ { x } = { A }
Theorem	bj-sbel1 32900*	Version of sbcel1g 3987 when substituting a set. (Note: one could have a corresponding version of sbcel12 3983 when substituting a set, but the point here is that the antecedent of sbcel1g 3987 is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018.)
|- ( [ y / x ] A e. B <-> [_ y / x ]_ A e. B )