P. 369 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36801-36900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-nfs1v 36801*	Version of nfsb2 2481 with a disjoint variable condition, which does not require ax-13 2370, and removal of ax-13 2370 from nfs1v 2157. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	bj-hbsb2av 36802*	Version of hbsb2a 2482 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-hbsb3v 36803*	Version of hbsb3 2485 with a disjoint variable condition, which does not require ax-13 2370. (Remark: the unbundled version of nfs1 2486 is given by bj-nfs1v 36801.) (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfsab1 36804*	Remove dependency on ax-13 2370 from nfsab1 2715. UPDATE / TODO: nfsab1 2715 does not use ax-13 2370 either anymore; bj-nfsab1 36804 is shorter than nfsab1 2715 but uses ax-12 2178. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	bj-dtrucor2v 36805*	Version of dtrucor2 5327 with a disjoint variable condition, which does not require ax-13 2370 (nor ax-4 1809, ax-5 1910, ax-7 2008, ax-12 2178). (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → 𝑥 ≠ 𝑦)    ⇒   ⊢ (𝜑 ∧ ¬ 𝜑)
21.19.4.13  Distinct var metavariables The closed formula ∀𝑥∀𝑦𝑥 = 𝑦 approximately means that the var metavariables 𝑥 and 𝑦 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 36806	Biconditional version of a form of hbae 2429 with commuted quantifiers, not requiring ax-11 2158. (Contributed by BJ, 12-Dec-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑧 𝑥 = 𝑦)
Theorem	bj-hbaeb 36807	Biconditional version of hbae 2429. (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	bj-hbnaeb 36808	Biconditional version of hbnae 2430 (to replace it?). (Contributed by BJ, 6-Oct-2018.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	bj-dvv 36809	A special instance of bj-hbaeb2 36806. A lemma for distinct var metavariables. Note that the right-hand side is a closed formula (a sentence). (Contributed by BJ, 6-Oct-2018.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑦 𝑥 = 𝑦)
21.19.4.14  Around ~ equsal As a rule of thumb, if a theorem of the form ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜒 ↔ 𝜃) is in the database, and the "more precise" theorems ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜒 → 𝜃) and ⊢ (𝜓 → 𝜑) ⇒ ⊢ (𝜃 → 𝜒) also hold (see bj-bisym 36578), then they should be added to the database. The present case is similar. Similar additions can be done regarding equsex 2416 (and equsalh 2418 and equsexh 2419). Even if only one of these two theorems holds, it should be added to the database.
Theorem	bj-equsal1t 36810	Duplication of wl-equsal1t 37530, with shorter proof. If one imposes a disjoint variable condition on x,y , then one can use alequexv 2001 and reduce axiom dependencies, and similarly for the following theorems. Note: wl-equsalcom 37531 is also interesting. (Contributed by BJ, 6-Oct-2018.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑))
Theorem	bj-equsal1ti 36811	Inference associated with bj-equsal1t 36810. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)
Theorem	bj-equsal1 36812	One direction of equsal 2415. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜓)
Theorem	bj-equsal2 36813	One direction of equsal 2415. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓))
Theorem	bj-equsal 36814	Shorter proof of equsal 2415. (Contributed by BJ, 30-Sep-2018.) Proof modification is discouraged to avoid using equsal 2415, but "min */exc equsal" is ok. (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
21.19.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 36815	Closed form of stdpc5 2209. (Possible to place it before 19.21t 2207 and use it to prove 19.21t 2207). (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-stdpc5 36816	More direct proof of stdpc5 2209. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
Theorem	2stdpc5 36817	A double stdpc5 2209 (one direction of PM*11.3). See also 2stdpc4 2071 and 19.21vv 44365. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	bj-19.21t0 36818	Proof of 19.21t 2207 from stdpc5t 36815. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	exlimii 36819	Inference associated with exlimi 2218. Inferring a theorem when it is implied by an antecedent which may be true. (Contributed by BJ, 15-Sep-2018.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → 𝜓)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜓
Theorem	ax11-pm 36820	Proof of ax-11 2158 similar to PM's proof of alcom 2160 (PM*11.2). For a proof closer to PM's proof, see ax11-pm2 36824. Axiom ax-11 2158 is used in the proof only through nfa2 2177. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	ax6er 36821	Commuted form of ax6e 2381. (Could be placed right after ax6e 2381). (Contributed by BJ, 15-Sep-2018.)
⊢ ∃𝑥 𝑦 = 𝑥
Theorem	exlimiieq1 36822	Inferring a theorem when it is implied by an equality which may be true. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	exlimiieq2 36823	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.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	ax11-pm2 36824*	Proof of ax-11 2158 from the standard axioms of predicate calculus, similar to PM's proof of alcom 2160 (PM*11.2). This proof requires that 𝑥 and 𝑦 be distinct. Axiom ax-11 2158 is used in the proof only through nfal 2322, nfsb 2521, sbal 2170, sb8 2515. See also ax11-pm 36820. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
21.19.4.16  Alternate definition of substitution
Theorem	bj-sbsb 36825	Biconditional showing two possible (dual) definitions of substitution df-sb 2066 not using dummy variables. (Contributed by BJ, 19-Mar-2021.)
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))
Theorem	bj-dfsb2 36826	Alternate (dual) definition of substitution df-sb 2066 not using dummy variables. (Contributed by BJ, 19-Mar-2021.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))
21.19.4.17  Lemmas for substitution
Theorem	bj-sbf3 36827	Substitution has no effect on a bound variable (existential quantifier case); see sbf2 2272. (Contributed by BJ, 2-May-2019.)
⊢ ([𝑦 / 𝑥]∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-sbf4 36828	Substitution has no effect on a bound variable (nonfreeness case); see sbf2 2272. (Contributed by BJ, 2-May-2019.)
⊢ ([𝑦 / 𝑥]Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜑)
21.19.4.18  Existential uniqueness
Theorem	bj-eu3f 36829*	Version of eu3v 2563 where the disjoint variable condition is replaced with a nonfreeness 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 2563. (Contributed by NM, 8-Jul-1994.) (Proof shortened by BJ, 31-May-2019.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
21.19.4.19  First-order logic: miscellaneous Miscellaneous theorems of first-order logic.
Theorem	bj-sblem1 36830*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜒)))
Theorem	bj-sblem2 36831*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝜑 → (𝜒 → 𝜓)) → ((∃𝑥𝜑 → 𝜒) → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-sblem 36832*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝜑 → (𝜓 ↔ 𝜒)) → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜒)))
Theorem	bj-sbievw1 36833*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → 𝜓))
Theorem	bj-sbievw2 36834*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ ([𝑦 / 𝑥](𝜓 → 𝜑) → (𝜓 → [𝑦 / 𝑥]𝜑))
Theorem	bj-sbievw 36835*	Lemma for substitution. Closed form of equsalvw 2004 and sbievw 2094. (Contributed by BJ, 23-Jul-2023.)
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
Theorem	bj-sbievv 36836	Version of sbie 2500 with a second nonfreeness hypothesis and shorter proof. (Contributed by BJ, 18-Jul-2023.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
Theorem	bj-moeub 36837	Uniqueness is equivalent to existence being equivalent to unique existence. (Contributed by BJ, 14-Oct-2022.)
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 ↔ ∃!𝑥𝜑))
Theorem	bj-sbidmOLD 36838	Obsolete proof of sbidm 2508 temporarily kept here to check it gives no additional insight. (Contributed by NM, 8-Mar-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	bj-dvelimdv 36839*	Deduction form of dvelim 2449 with disjoint variable conditions. Uncurried (imported) form of bj-dvelimdv1 36840. Typically, 𝑧 is a fresh variable used for the implicit substitution hypothesis that results in 𝜒 (namely, 𝜓 can be thought as 𝜓(𝑥, 𝑦) and 𝜒 as 𝜓(𝑥, 𝑧)). So the theorem says that if x is effectively free in 𝜓(𝑥, 𝑧), then if x and y are not the same variable, then 𝑥 is also effectively free in 𝜓(𝑥, 𝑦), in a context 𝜑. One can weaken the implicit substitution hypothesis by adding the antecedent 𝜑 but this typically does not make the theorem much more useful. Similarly, one could use nonfreeness hypotheses instead of disjoint variable conditions but since this result is typically used when 𝑧 is a dummy variable, this would not be of much benefit. One could also remove DV (𝑥, 𝑧) since in the proof nfv 1914 can be replaced with nfal 2322 followed by nfn 1857. Remark: nfald 2327 uses ax-11 2158; it might be possible to inline and use ax11w 2131 instead, but there is still a use via 19.12 2326 anyway. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜓))    ⇒   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)
Theorem	bj-dvelimdv1 36840*	Curried (exported) form of bj-dvelimdv 36839 (of course, one is directly provable from the other, but we keep this proof for illustration purposes). (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓))
Theorem	bj-dvelimv 36841*	A version of dvelim 2449 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑧 = 𝑦 → (𝜓 ↔ 𝜑))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)
Theorem	bj-nfeel2 36842*	Nonfreeness in a membership statement. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 ∈ 𝑧)
Theorem	bj-axc14nf 36843	Proof of a version of axc14 2461 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧 𝑥 ∈ 𝑦))
Theorem	bj-axc14 36844	Alternate proof of axc14 2461 (even when inlining the above results, this gives a shorter proof). (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Theorem	mobidvALT 36845*	Alternate proof of mobidv 2542 directly from its analogues albidv 1920 and exbidv 1921, using deduction style. Note the proof structure, similar to mobi 2540. (Contributed by Mario Carneiro, 7-Oct-2016.) Reduce axiom dependencies and shorten proof. Remove dependency on ax-6 1967, ax-7 2008, ax-12 2178 by adapting proof of mobid 2543. (Revised by BJ, 26-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Theorem	sbn1ALT 36846	Alternate proof of sbn1 2108, not using the false constant. (Contributed by BJ, 18-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ([𝑡 / 𝑥] ¬ 𝜑 → ¬ [𝑡 / 𝑥]𝜑)
21.19.5  Set theory
21.19.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 2701, df-clab 2708, df-cleq 2721, df-clel 2803 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 in set.mm. It states: every formula in the language of FOL + ∈ + class terms, but without class variables, is provably equivalent (over {FOL, ax-ext 2701, df-clab 2708, df-cleq 2721, df-clel 2803 }) to a formula in the language of FOL + ∈ (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 six following forms: for equality, 𝑥 = {𝑦 ∣ 𝜑}, {𝑥 ∣ 𝜑} = 𝑦, {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}, and for membership, 𝑦 ∈ {𝑥 ∣ 𝜑}, {𝑥 ∣ 𝜑} ∈ 𝑦, {𝑥 ∣ 𝜑} ∈ {𝑦 ∣ 𝜓}. These cases are dealt with by eliminable-veqab 36854, eliminable-abeqv 36855, eliminable-abeqab 36856, eliminable-velab 36853, eliminable-abelv 36857, eliminable-abelab 36858 respectively, which are all proved from {FOL, ax-ext 2701, df-clab 2708, df-cleq 2721, df-clel 2803 }. (Details on the proof of the above six theorems. To understand how they were systematically proved, look at the theorems "eliminablei" below, which are special instances of df-clab 2708, dfcleq 2722 (proved from {FOL, ax-ext 2701, df-cleq 2721 }), and dfclel 2804 (proved from {FOL, df-clel 2803 }). 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 36848, eliminable2b 36849 and eliminable3a 36851, 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 1539, 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 𝑦 ∈ {𝑥 ∣ 𝜑}, then df-clab 2708 is sufficient (over FOL) to eliminate class terms, and if the original formula has only class terms appearing in atomic formulas of the form 𝑦 ∈ {𝑥 ∣ 𝜑} and equalities, then df-clab 2708, ax-ext 2701 and df-cleq 2721 are sufficient (over FOL) to eliminate class terms. To prove that { df-clab 2708, df-cleq 2721, df-clel 2803 } provides a definitional extension of {FOL, ax-ext 2701 }, one needs to prove both 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 2708, df-cleq 2721, df-clel 2803 }. 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 2701 }. 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 2708, df-cleq 2721, df-clel 2803 }. It involves a careful case study on the structure of the proof tree.
Theorem	eliminable1 36847	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.)
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
Theorem	eliminable2a 36848*	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.)
⊢ (𝑥 = {𝑦 ∣ 𝜑} ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ {𝑦 ∣ 𝜑}))
Theorem	eliminable2b 36849*	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.)
⊢ ({𝑥 ∣ 𝜑} = 𝑦 ↔ ∀𝑧(𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ 𝑦))
Theorem	eliminable2c 36850*	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.)
⊢ ({𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} ↔ ∀𝑧(𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓}))
Theorem	eliminable3a 36851*	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.)
⊢ ({𝑥 ∣ 𝜑} ∈ 𝑦 ↔ ∃𝑧(𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 ∈ 𝑦))
Theorem	eliminable3b 36852*	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.)
⊢ ({𝑥 ∣ 𝜑} ∈ {𝑦 ∣ 𝜓} ↔ ∃𝑧(𝑧 = {𝑥 ∣ 𝜑} ∧ 𝑧 ∈ {𝑦 ∣ 𝜓}))
Theorem	eliminable-velab 36853	A theorem used to prove the base case of the Eliminability Theorem (see section comment): variable belongs to abstraction. (Contributed by BJ, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
Theorem	eliminable-veqab 36854*	A theorem used to prove the base case of the Eliminability Theorem (see section comment): variable equals abstraction. (Contributed by BJ, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = {𝑦 ∣ 𝜑} ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ [𝑧 / 𝑦]𝜑))
Theorem	eliminable-abeqv 36855*	A theorem used to prove the base case of the Eliminability Theorem (see section comment): abstraction equals variable. (Contributed by BJ, 30-Apr-2024.) Beware not to use symmetry of class equality. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ({𝑥 ∣ 𝜑} = 𝑦 ↔ ∀𝑧([𝑧 / 𝑥]𝜑 ↔ 𝑧 ∈ 𝑦))
Theorem	eliminable-abeqab 36856*	A theorem used to prove the base case of the Eliminability Theorem (see section comment): abstraction equals abstraction. (Contributed by BJ, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ({𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} ↔ ∀𝑧([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓))
Theorem	eliminable-abelv 36857*	A theorem used to prove the base case of the Eliminability Theorem (see section comment): abstraction belongs to variable. (Contributed by BJ, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ({𝑥 ∣ 𝜑} ∈ 𝑦 ↔ ∃𝑧(∀𝑡(𝑡 ∈ 𝑧 ↔ [𝑡 / 𝑥]𝜑) ∧ 𝑧 ∈ 𝑦))
Theorem	eliminable-abelab 36858*	A theorem used to prove the base case of the Eliminability Theorem (see section comment): abstraction belongs to abstraction. (Contributed by BJ, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ({𝑥 ∣ 𝜑} ∈ {𝑦 ∣ 𝜓} ↔ ∃𝑧(∀𝑡(𝑡 ∈ 𝑧 ↔ [𝑡 / 𝑥]𝜑) ∧ [𝑧 / 𝑦]𝜓))
21.19.5.2  Classes without the axiom of extensionality A few results about classes can be proved without using ax-ext 2701. One could move all theorems from cab 2707 to df-clel 2803 (except for dfcleq 2722 and cvjust 2723) 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 2721. Note that without ax-ext 2701, the $a-statements df-clab 2708, df-cleq 2721, and df-clel 2803 are no longer eliminable (see previous section) (but PROBABLY df-clab 2708 is still conservative , while df-cleq 2721 and df-clel 2803 are not). This is not a reason not to study what is provable with them but without ax-ext 2701, in order to gauge their strengths more precisely. Before that subsection, a subsection "The membership predicate" could group the statements with ∈ that are currently in the FOL part (including wcel 2109, wel 2110, ax-8 2111, ax-9 2119). Remark: the weakening of eleq1 2816 / eleq2 2817 to eleq1w 2811 / eleq2w 2812 can also be done with eleq1i 2819, eqeltri 2824, eqeltrri 2825, eleq1a 2823, eleq1d 2813, eqeltrd 2828, eqeltrrd 2829, eqneltrd 2848, eqneltrrd 2849, nelneq 2852. Remark: possibility to remove dependency on ax-10 2142, ax-11 2158, ax-13 2370 from nfcri 2883 and theorems using it if one adds a disjoint variable condition (that theorem is typically used with dummy variables, so the disjoint variable condition addition is not very restrictive), and then shorten nfnfc 2904.
Theorem	bj-denoteslem 36859*	Duplicate of issettru 2806 and bj-issettruALTV 36861. Lemma for bj-denotesALTV 36860. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-denotesALTV 36860*	Moved to main as iseqsetv-clel 2807 and kept for the comments. This would be the justification theorem for the definition of the unary predicate "E!" by ⊢ ( E! 𝐴 ↔ ∃𝑥𝑥 = 𝐴) which could be interpreted as "𝐴 exists" (as a set) or "𝐴 denotes" (in the sense of free logic). A shorter proof using bitri 275 (to add an intermediate proposition ∃𝑧𝑧 = 𝐴 with a fresh 𝑧), cbvexvw 2037, and eqeq1 2733, requires the core axioms and { ax-9 2119, ax-ext 2701, df-cleq 2721 } whereas this proof requires the core axioms and { ax-8 2111, df-clab 2708, df-clel 2803 }. Theorem bj-issetwt 36863 proves that "existing" is equivalent to being a member of a class abstraction. It also requires, with the present proof, { ax-8 2111, df-clab 2708, df-clel 2803 } (whereas with the shorter proof from cbvexvw 2037 and eqeq1 2733 it would require { ax-8 2111, ax-9 2119, ax-ext 2701, df-clab 2708, df-cleq 2721, df-clel 2803 }). That every class is equal to a class abstraction is proved by abid1 2864, which requires { ax-8 2111, ax-9 2119, ax-ext 2701, df-clab 2708, df-cleq 2721, df-clel 2803 }. Note that there is no disjoint variable condition on 𝑥, 𝑦 but the theorem does not depend on ax-13 2370. Actually, the proof depends only on the logical axioms ax-1 6 through ax-7 2008 and sp 2184. 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 nonexistent objects. This analogy should not be taken too far, since here there are no equality axioms for classes: these are derived from ax-ext 2701 and df-cleq 2721 (e.g., eqid 2729 and eqeq1 2733). In particular, one cannot even prove ⊢ ∃𝑥𝑥 = 𝐴 ⇒ ⊢ 𝐴 = 𝐴 without ax-ext 2701 and df-cleq 2721. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	bj-issettruALTV 36861*	Moved to main as issettru 2806 and kept for the comments. Weak version of isset 3461 without ax-ext 2701. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-elabtru 36862	This is as close as we can get to proving extensionality for "the" "universal" class without ax-ext 2701. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ {𝑥 ∣ ⊤} ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-issetwt 36863*	Closed form of bj-issetw 36864. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴))
Theorem	bj-issetw 36864*	The closest one can get to isset 3461 without using ax-ext 2701. See also vexw 2713. Note that the only disjoint variable condition is between 𝑦 and 𝐴. From there, one can prove isset 3461 using eleq2i 2820 (which requires ax-ext 2701 and df-cleq 2721). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	bj-issetiv 36865*	Version of bj-isseti 36866 with a disjoint variable condition on 𝑥, 𝑉. The hypothesis uses 𝑉 instead of V for extra generality. This is indeed more general than isseti 3465 as long as elex 3468 is not available (and the non-dependence of bj-issetiv 36865 on special properties of the universal class V is obvious). Prefer its use over bj-isseti 36866 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∃𝑥 𝑥 = 𝐴
Theorem	bj-isseti 36866*	Version of isseti 3465 with a class variable 𝑉 in the hypothesis instead of V for extra generality. This is indeed more general than isseti 3465 as long as elex 3468 is not available (and the non-dependence of bj-isseti 36866 on special properties of the universal class V is obvious). Use bj-issetiv 36865 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∃𝑥 𝑥 = 𝐴
Theorem	bj-ralvw 36867	A weak version of ralv 3474 not using ax-ext 2701 (nor df-cleq 2721, df-clel 2803, df-v 3449), and only core FOL axioms. See also bj-rexvw 36868. The analogues for reuv 3476 and rmov 3477 are not proved. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∀𝑥𝜑)
Theorem	bj-rexvw 36868	A weak version of rexv 3475 not using ax-ext 2701 (nor df-cleq 2721, df-clel 2803, df-v 3449), and only core FOL axioms. See also bj-ralvw 36867. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-rababw 36869	A weak version of rabab 3478 not using df-clel 2803 nor df-v 3449 (but requiring ax-ext 2701) nor ax-12 2178. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ {𝑥 ∈ {𝑦 ∣ 𝜓} ∣ 𝜑} = {𝑥 ∣ 𝜑}
Theorem	bj-rexcom4bv 36870*	Version of rexcom4b 3479 and bj-rexcom4b 36871 with a disjoint variable condition on 𝑥, 𝑉, hence removing dependency on df-sb 2066 and df-clab 2708 (so that it depends on df-clel 2803 and df-rex 3054 only on top of first-order logic). Prefer its use over bj-rexcom4b 36871 when sufficient (in particular when 𝑉 is substituted for V). Note the 𝑉 in the hypothesis instead of V. (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ 𝐵 ∈ 𝑉    ⇒   ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑)
Theorem	bj-rexcom4b 36871*	Remove from rexcom4b 3479 dependency on ax-ext 2701 and ax-13 2370 (and on df-or 848, df-cleq 2721, df-nfc 2878, df-v 3449). The hypothesis uses 𝑉 instead of V (see bj-isseti 36866 for the motivation). Use bj-rexcom4bv 36870 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝐵 ∈ 𝑉    ⇒   ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑)
Theorem	bj-ceqsalt0 36872	The FOL content of ceqsalt 3481. Lemma for bj-ceqsalt 36874 and bj-ceqsaltv 36875. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜃 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥𝜃) → (∀𝑥(𝜃 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalt1 36873	The FOL content of ceqsalt 3481. Lemma for bj-ceqsalt 36874 and bj-ceqsaltv 36875. TODO: consider removing if it does not add anything to bj-ceqsalt0 36872. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
⊢ (𝜃 → ∃𝑥𝜒)    ⇒   ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜒 → (𝜑 ↔ 𝜓)) ∧ 𝜃) → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalt 36874*	Remove from ceqsalt 3481 dependency on ax-ext 2701 (and on df-cleq 2721 and df-v 3449). Note: this is not doable with ceqsralt 3482 (or ceqsralv 3488), which uses eleq1 2816, but the same dependence removal is possible for ceqsalg 3483, ceqsal 3485, ceqsalv 3487, cgsexg 3492, cgsex2g 3493, cgsex4g 3494, ceqsex 3496, ceqsexv 3498, ceqsex2 3501, ceqsex2v 3502, ceqsex3v 3503, ceqsex4v 3504, ceqsex6v 3505, ceqsex8v 3506, gencbvex 3507 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3508, gencbval 3509, vtoclgft 3518 (it uses Ⅎ, whose justification nfcjust 2877 does not use ax-ext 2701) and several other vtocl* theorems (see for instance bj-vtoclg1f 36906). See also bj-ceqsaltv 36875. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsaltv 36875*	Version of bj-ceqsalt 36874 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2066 and df-clab 2708. Prefer its use over bj-ceqsalt 36874 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalg0 36876	The FOL content of ceqsalg 3483. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜒 → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalg 36877*	Remove from ceqsalg 3483 dependency on ax-ext 2701 (and on df-cleq 2721 and df-v 3449). See also bj-ceqsalgv 36879. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgALT 36878*	Alternate proof of bj-ceqsalg 36877. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgv 36879*	Version of bj-ceqsalg 36877 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2066 and df-clab 2708. Prefer its use over bj-ceqsalg 36877 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgvALT 36880*	Alternate proof of bj-ceqsalgv 36879. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsal 36881*	Remove from ceqsal 3485 dependency on ax-ext 2701 (and on df-cleq 2721, df-v 3449, df-clab 2708, df-sb 2066). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	bj-ceqsalv 36882*	Remove from ceqsalv 3487 dependency on ax-ext 2701 (and on df-cleq 2721, df-v 3449, df-clab 2708, df-sb 2066). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	bj-spcimdv 36883*	Remove from spcimdv 3559 dependency on ax-9 2119, ax-10 2142, ax-11 2158, ax-13 2370, ax-ext 2701, df-cleq 2721 (and df-nfc 2878, df-v 3449, df-or 848, df-tru 1543, df-nf 1784). For an even more economical version, see bj-spcimdvv 36884. (Contributed by BJ, 30-Nov-2020.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	bj-spcimdvv 36884*	Remove from spcimdv 3559 dependency on ax-7 2008, ax-8 2111, ax-10 2142, ax-11 2158, ax-12 2178 ax-13 2370, ax-ext 2701, df-cleq 2721, df-clab 2708 (and df-nfc 2878, df-v 3449, df-or 848, df-tru 1543, df-nf 1784) at the price of adding a disjoint variable condition on 𝑥, 𝐵 (but in usages, 𝑥 is typically a dummy, hence fresh, variable). For the version without this disjoint variable condition, see bj-spcimdv 36883. (Contributed by BJ, 3-Nov-2021.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
21.19.5.3  Characterization among sets versus among classes
Theorem	elelb 36885	Equivalence between two common ways to characterize elements of a class 𝐵: the LHS says that sets are elements of 𝐵 if and only if they satisfy 𝜑 while the RHS says that classes are elements of 𝐵 if and only if they are sets and satisfy 𝜑. Therefore, the LHS is a characterization among sets while the RHS is a characterization among classes. Note that the LHS is often formulated using a class variable instead of the universe V while this is not possible for the RHS (apart from using 𝐵 itself, which would not be very useful). (Contributed by BJ, 26-Feb-2023.)
⊢ ((𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ 𝜑)) ↔ (𝐴 ∈ 𝐵 ↔ (𝐴 ∈ V ∧ 𝜑)))
Theorem	bj-pwvrelb 36886	Characterization of the elements of the powerclass of the cartesian square of the universal class: they are exactly the sets which are binary relations. (Contributed by BJ, 16-Dec-2023.)
⊢ (𝐴 ∈ 𝒫 (V × V) ↔ (𝐴 ∈ V ∧ Rel 𝐴))
21.19.5.4  The nonfreeness quantifier for classes In this section, we prove the symmetry of the nonfreeness quantifier for classes.
Theorem	bj-nfcsym 36887	The nonfreeness quantifier for classes defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 5330 with additional axioms; see also nfcv 2891). This could be proved from aecom 2425 and nfcvb 5331 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 2735 instead of equcomd 2019; removing dependency on ax-ext 2701 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2911, eleq2d 2814 (using elequ2 2124), nfcvf 2918, dvelimc 2917, dvelimdc 2916, nfcvf2 2919. (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥)
21.19.5.5  Lemmas for class substitution Some useful theorems for dealing with substitutions: sbbi 2307, sbcbig 3805, sbcel1g 4379, sbcel2 4381, sbcel12 4374, sbceqg 4375, csbvarg 4397.
Theorem	bj-sbeqALT 36888*	Substitution in an equality (use the more general version bj-sbeq 36889 instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵)
Theorem	bj-sbeq 36889	Distribute proper substitution through an equality relation. (See sbceqg 4375). (Contributed by BJ, 6-Oct-2018.)
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵)
Theorem	bj-sbceqgALT 36890	Distribute proper substitution through an equality relation. Alternate proof of sbceqg 4375. (Contributed by BJ, 6-Oct-2018.) Proof modification is discouraged to avoid using sbceqg 4375, but the Metamath program "MM-PA> MINIMIZE_WITH * / EXCEPT sbceqg" command is ok. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))
Theorem	bj-csbsnlem 36891*	Lemma for bj-csbsn 36892 (in this lemma, 𝑥 cannot occur in 𝐴). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴}
Theorem	bj-csbsn 36892	Substitution in a singleton. (Contributed by BJ, 6-Oct-2018.)
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴}
Theorem	bj-sbel1 36893*	Version of sbcel1g 4379 when substituting a set. (Note: one could have a corresponding version of sbcel12 4374 when substituting a set, but the point here is that the antecedent of sbcel1g 4379 is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018.)
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ 𝐵)
Theorem	bj-abv 36894	The class of sets verifying a tautology is the universal class. (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → {𝑥 ∣ 𝜑} = V)
Theorem	bj-abvALT 36895	Alternate version of bj-abv 36894; shorter but uses ax-8 2111. (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → {𝑥 ∣ 𝜑} = V)
Theorem	bj-ab0 36896	The class of sets verifying a falsity is the empty set (closed form of abf 4369). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 ¬ 𝜑 → {𝑥 ∣ 𝜑} = ∅)
Theorem	bj-abf 36897	Shorter proof of abf 4369 (which should be kept as abfALT). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ ¬ 𝜑    ⇒   ⊢ {𝑥 ∣ 𝜑} = ∅
Theorem	bj-csbprc 36898	More direct proof of csbprc 4372 (fewer essential steps). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)
21.19.5.6  Removing some axiom requirements and disjoint variable conditions
Theorem	bj-exlimvmpi 36899*	A Fol lemma (exlimiv 1930 followed by mpi 20). (Contributed by BJ, 2-Jul-2022.) (Proof modification is discouraged.)
⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpi 36900	Lemma for bj-vtoclg1f1 36905 (an instance of this lemma is a version of bj-vtoclg1f1 36905 where 𝑥 and 𝑦 are identified). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)