P. 321 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32001-32100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-equsal 32001	Shorter proof of equsal 2279. (Contributed by BJ, 30-Sep-2018.) Proof modification is discouraged to avoid using equsal 2279, but "min */exc equsal" is ok. (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
21.14.4.16  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 32002	Closed form of stdpc5 2063. (Possible to place it before 19.21t 2061 and use it to prove 19.21t 2061). (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-stdpc5 32003	More direct proof of stdpc5 2063. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
Theorem	2stdpc5 32004	A double stdpc5 2063 (one direction of PM*11.3). See also 2stdpc4 2342 and 19.21vv 37597. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	bj-19.21t 32005	Proof of 19.21t 2061 from stdpc5t 32002. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	exlimii 32006	Inference associated with exlimi 2073. Inferring a theorem when it is implied by an antecedent which may be true. (Contributed by BJ, 15-Sep-2018.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → 𝜓)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜓
Theorem	ax11-pm 32007	Proof of ax-11 2021 similar to PM's proof of alcom 2024 (PM*11.2). For a proof closer to PM's proof, see ax11-pm2 32011. Axiom ax-11 2021 is used in the proof only through nfa2 2027. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	ax6er 32008	Another form of ax6e 2238. ( Could be placed right after ax6e 2238). (Contributed by BJ, 15-Sep-2018.)
⊢ ∃𝑥 𝑦 = 𝑥
Theorem	exlimiieq1 32009	Inferring a theorem when it is implied by an equality which may be true. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	exlimiieq2 32010	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 32011*	Proof of ax-11 2021 from the standard axioms of predicate calculus, similar to PM's proof of alcom 2024 (PM*11.2). This proof requires that 𝑥 and 𝑦 be distinct. Axiom ax-11 2021 is used in the proof only through nfal 2139, nfsb 2428, sbal 2450, sb8 2412. See also ax11-pm 32007. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
21.14.4.17  Alternate definition of substitution
Theorem	bj-sbsb 32012	Biconditional showing two possible (dual) definitions of substitution df-sb 1868 not using dummy variables. (Contributed by BJ, 19-Mar-2021.)
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))
Theorem	bj-dfsb2 32013	Alternate (dual) definition of substitution df-sb 1868 not using dummy variables. (Contributed by BJ, 19-Mar-2021.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))
21.14.4.18  Lemmas for substitution
Theorem	bj-sbf3 32014	Substitution has no effect on a bound variabe (existential quantifier case); see sbf2 2370. (Contributed by BJ, 2-May-2019.)
⊢ ([𝑦 / 𝑥]∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-sbf4 32015	Substitution has no effect on a bound variabe (non-freeness case); see sbf2 2370. (Contributed by BJ, 2-May-2019.)
⊢ ([𝑦 / 𝑥]Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜑)
Theorem	bj-sbnf 32016*	Move non-free predicate in and out of substitution; see sbal 2450 and sbex 2451. (Contributed by BJ, 2-May-2019.)
⊢ ([𝑧 / 𝑦]Ⅎ𝑥𝜑 ↔ Ⅎ𝑥[𝑧 / 𝑦]𝜑)
21.14.4.19  Existential uniqueness
Theorem	bj-eu3f 32017*	Version of eu3v 2486 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 2486. (Contributed by NM, 8-Jul-1994.) (Proof shortened by BJ, 31-May-2019.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
Theorem	bj-eumo0 32018*	Existential uniqueness implies "at most one." Used to be in the main part and deprecated in favor of eumo 2487 and mo2 2467. (Contributed by NM, 8-Jul-1994.) (Revised by BJ, 8-Jun-2019.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃!𝑥𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
21.14.4.20  First-logic: miscellaneous Miscellaneous theorems of first-order logic.
Theorem	bj-nfdiOLD 32019	Obsolete proof temporarily kept here in view of the change of nf5 2102 to df-nf 1701. (Contributed by NM, 8-Mar-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝜑)    ⇒   ⊢ Ⅎ𝑥𝜑
Theorem	bj-sbieOLD 32020	Obsolete proof 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-sbidmOLD 32021	Obsolete proof 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-mo3OLD 32022*	Obsolete proof 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-syl66ib 32023	A mixed syllogism inference derived from syl6ib 240. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜃 → 𝜏)    &   ⊢ (𝜏 ↔ 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	bj-nfbiit 32024	Closed form of nfbii 1770 (the label " nfbi 1821 " is taken for another result. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓))
Theorem	bj-nfimt 32025	Closed form of nfim 1813. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (Ⅎ𝑥𝜓 → Ⅎ𝑥(𝜑 → 𝜓)))
Theorem	bj-nfimt2 32026	Uncurried form of bj-nfimt 32025 and closed form of nfim 1813. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑 → 𝜓))
Theorem	bj-dvelimdv 32027*	Deduction form of dvelim 2325 with DV conditions. 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 weakend the implicit substitution hypothesis by adding the antecedent 𝜑 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 𝑧 is a dummy variable, this would not be of much benefit. One could also remove DV(z,x) since in the proof nfv 1830 can be replaced with nfal 2139 followed by nfn 1768. Remark: nfald 2151 uses ax-11 2021; it might be possible to inline and use ax11w 1994 instead, but there is still a use via 19.12 2150 anyway. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜓))    ⇒   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)
Theorem	bj-dvelimdv1 32028*	Curried form (exported form) of bj-dvelimdv 32027. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓))
Theorem	bj-dvelimv 32029*	A version of dvelim 2325 using the "non-free" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑧 = 𝑦 → (𝜓 ↔ 𝜑))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)
Theorem	bj-nfeel2 32030*	Non-freeness in an equality. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 ∈ 𝑧)
Theorem	bj-axc14nf 32031	Proof of a version of axc14 2360 using the "non-free" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧 𝑥 ∈ 𝑦))
Theorem	bj-axc14 32032	Alternate proof of axc14 2360 (even when inlining the above results, this gives a shorter proof). (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
21.14.5  Set theory
21.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 2590, df-clab 2597, df-cleq 2603, df-clel 2606 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 + ∈ + class terms, but without class variables, is provably equivalent (over {FOL, ax-ext 2590, df-clab 2597, df-cleq 2603, df-clel 2606 }) 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 following forms: for equality, 𝑥 = {𝑦 ∣ 𝜑}, {𝑥 ∣ 𝜑} = 𝑦, {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}, and for membership, 𝑦 ∈ {𝑥 ∣ 𝜑}, {𝑥 ∣ 𝜑} ∈ 𝑦, {𝑥 ∣ 𝜑} ∈ {𝑦 ∣ 𝜓}. These cases are dealt with by eliminable1 32033 and the following theorems of this section, which are special instances of df-clab 2597, dfcleq 2604 (proved from {FOL, ax-ext 2590, df-cleq 2603 }), and df-clel 2606. 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 32034, eliminable2b 32035 and eliminable3a 32037, 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 1474, 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 2597 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 2597, ax-ext 2590 and df-cleq 2603 are sufficient (over FOL) to eliminate class terms. To prove that { df-clab 2597, df-cleq 2603, df-clel 2606 } provides a definitional extension of {FOL, ax-ext 2590 }, 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 2597, df-cleq 2603, df-clel 2606 }. 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 2590 }. 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 2597, df-cleq 2603, df-clel 2606 }. It involves a careful case study on the structure of the proof tree.
Theorem	eliminable1 32033	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 32034*	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 32035*	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 32036*	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 32037*	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 32038*	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	bj-termab 32039*	Every class can be written as (is equal to) a class abstraction. cvjust 2605 is a special instance of it, but the present proof does not require ax-13 2234, contrary to cvjust 2605. This theorem requires ax-ext 2590, df-clab 2597, df-cleq 2603, df-clel 2606, 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 1474, cab 2596 and statements corresponding to defined class constructors. UPDATE: This theorem is (almost) abid2 2732 and bj-abid2 31970, though the present proof is shorter than a proof from bj-abid2 31970 and eqcomi 2619 (and is shorter than the proof of either); plus, it is of the same form as cvjust 2605 and such a basic statement deserves to be present in both forms. Note that bj-termab 32039 shortens the proof of abid2 2732, and shortens five proofs by a total of 72 bytes. Move it to Main as "abid1" proved from abbi2i 2725? Note also that this is the form in Quine, more than abid2 2732. (Contributed by BJ, 21-Oct-2019.) (Proof modification is discouraged.)
⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}
21.14.5.2  Classes without extensionality A few results about classes can be proved without using ax-ext 2590. One could move all theorems from cab 2596 to df-clel 2606 (except for dfcleq 2604 and cvjust 2605) 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 2603. Note that without ax-ext 2590, the $a-statements df-clab 2597, df-cleq 2603, and df-clel 2606 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 2590, 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 1977, wel 1978, ax-8 1979, ax-9 1986).
Theorem	bj-eleq1w 32040	Weaker version of eleq1 2676 (but more general than elequ1 1984) not depending on ax-ext 2590 (nor ax-12 2034 nor df-cleq 2603). Remark: this can also be done with eleq1i 2679, eqeltri 2684, eqeltrri 2685, eleq1a 2683, eleq1d 2672, eqeltrd 2688, eqeltrrd 2689, eqneltrd 2707, eqneltrrd 2708, nelneq 2712. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
Theorem	bj-eleq2w 32041	Weaker version of eleq2 2677 (but more general than elequ2 1991) not depending on ax-ext 2590 (nor ax-12 2034 nor df-cleq 2603). (Contributed by BJ, 29-Sep-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦))
Theorem	bj-clelsb3 32042*	Remove dependency on ax-ext 2590 (and df-cleq 2603) from clelsb3 2716. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ ([𝑥 / 𝑦]𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)
Theorem	bj-hblem 32043*	Remove dependency on ax-ext 2590 (and df-cleq 2603) from hblem 2718. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)    ⇒   ⊢ (𝑧 ∈ 𝐴 → ∀𝑥 𝑧 ∈ 𝐴)
Theorem	bj-nfcjust 32044*	Remove dependency on ax-ext 2590 (and df-cleq 2603 and ax-13 2234) from nfcjust 2739. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴 ↔ ∀𝑧Ⅎ𝑥 𝑧 ∈ 𝐴)
Theorem	bj-nfcrii 32045*	Remove dependency on ax-ext 2590 (and df-cleq 2603) from nfcrii 2744. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
Theorem	bj-nfcri 32046*	Remove dependency on ax-ext 2590 (and df-cleq 2603) from nfcri 2745. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
Theorem	bj-nfnfc 32047	Remove dependency on ax-ext 2590 (and df-cleq 2603) from nfnfc 2760. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥Ⅎ𝑦𝐴
Theorem	bj-vexwt 32048	Closed form of bj-vexw 32049. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) Use bj-vexwvt 32050 instead when sufficient. (New usage is discouraged.)
⊢ (∀𝑥𝜑 → 𝑦 ∈ {𝑥 ∣ 𝜑})
Theorem	bj-vexw 32049	If 𝜑 is a theorem, then any set belongs to the class {𝑥 ∣ 𝜑}. Therefore, {𝑥 ∣ 𝜑} is "a" universal class. This is the closest one can get to defining a universal class, or proving vex 3176, without using ax-ext 2590. Note that this theorem has no dv condition and does not use df-clel 2606 nor df-cleq 2603 either: only first-order logic and df-clab 2597. Without ax-ext 2590, one cannot define "the" universal class, since one could not prove for instance the justification theorem {𝑥 ∣ ⊤} = {𝑦 ∣ ⊤} (see vjust 3174). Indeed, in order to prove any equality of classes, one needs df-cleq 2603, which has ax-ext 2590 as a hypothesis. Therefore, the classes {𝑥 ∣ ⊤}, {𝑦 ∣ (𝜑 → 𝜑)}, {𝑧 ∣ (∀𝑡𝑡 = 𝑡 → ∀𝑡𝑡 = 𝑡)} and countless others are all universal classes whose equality one cannot prove without ax-ext 2590. See also bj-issetw 32054. A version with a dv condition between 𝑥 and 𝑦 and not requiring ax-13 2234 is proved as bj-vexwv 32051, while the degenerate instance is a simple consequence of abid 2598. (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.) Use bj-vexwv 32051 instead when sufficient. (New usage is discouraged.)
⊢ 𝜑    ⇒   ⊢ 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	bj-vexwvt 32050*	Closed form of bj-vexwv 32051 and version of bj-vexwt 32048 with a dv condition, which does not require ax-13 2234. (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → 𝑦 ∈ {𝑥 ∣ 𝜑})
Theorem	bj-vexwv 32051*	Version of bj-vexw 32049 with a dv condition, which does not require ax-13 2234. The degenerate instance of bj-vexw 32049 is a simple consequence of abid 2598 (which does not depend on ax-13 2234 either). (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜑    ⇒   ⊢ 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	bj-denotes 32052*	This would be the justification for the definition of the unary predicate "E!" by ⊢ ( E! 𝐴 ↔ ∃𝑥𝑥 = 𝐴) which could be interpreted as "𝐴 exists" or "𝐴 denotes". It is interesting that this justification can be proved without ax-ext 2590 nor df-cleq 2603 (but of course using df-clab 2597 and df-clel 2606). Once extensionality is postulated, then isset 3180 will prove that "existing" (as a set) is equivalent to being a member of a class. Note that there is no dv condition on 𝑥, 𝑦 but the theorem does not depend on ax-13 2234. Actually, the proof depends only on ax-1--7 and sp 2041. 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 2590 (e.g., eqid 2610). In particular, one cannot even prove ⊢ ∃𝑥𝑥 = 𝐴 ⇒ ⊢ 𝐴 = 𝐴. With ax-ext 2590, the present theorem is obvious from cbvexv 2263 and eqeq1 2614 (in free logic, the same proof holds since one has equality axioms for terms). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	bj-issetwt 32053*	Closed form of bj-issetw 32054. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴))
Theorem	bj-issetw 32054*	The closest one can get to isset 3180 without using ax-ext 2590. See also bj-vexw 32049. Note that the only dv condition is between 𝑦 and 𝐴. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	bj-elissetv 32055*	Version of bj-elisset 32056 with a dv condition on 𝑥, 𝑉. This proof uses only df-ex 1696, ax-gen 1713, ax-4 1728 and df-clel 2606 on top of propositional calculus. Prefer its use over bj-elisset 32056 when sufficient. (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
Theorem	bj-elisset 32056*	Remove from elisset 3188 dependency on ax-ext 2590 (and on df-cleq 2603 and df-v 3175). This proof uses only df-clab 2597 and df-clel 2606 on top of first-order logic. It only requires ax-1--7 and sp 2041. Use bj-elissetv 32055 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
Theorem	bj-issetiv 32057*	Version of bj-isseti 32058 with a dv condition on 𝑥, 𝑉. This proof uses only df-ex 1696, ax-gen 1713, ax-4 1728 and df-clel 2606 on top of propositional calculus. Prefer its use over bj-isseti 32058 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∃𝑥 𝑥 = 𝐴
Theorem	bj-isseti 32058*	Remove from isseti 3182 dependency on ax-ext 2590 (and on df-cleq 2603 and df-v 3175). This proof uses only df-clab 2597 and df-clel 2606 on top of first-order logic. It only uses ax-12 2034 among the auxiliary logical axioms. The hypothesis uses 𝑉 instead of V for extra generality. This is indeed more general as long as elex 3185 is not available. Use bj-issetiv 32057 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∃𝑥 𝑥 = 𝐴
Theorem	bj-ralvw 32059	A weak version of ralv 3192 not using ax-ext 2590 (nor df-cleq 2603, df-clel 2606, df-v 3175), but using ax-13 2234. For the sake of illustration, the next theorem bj-rexvwv 32060, a weak version of rexv 3193, has a dv condition and avoids dependency on ax-13 2234, while the analogues for reuv 3194 and rmov 3195 are not proved. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∀𝑥𝜑)
Theorem	bj-rexvwv 32060*	A weak version of rexv 3193 not using ax-ext 2590 (nor df-cleq 2603, df-clel 2606, df-v 3175) with an additional dv condition to avoid dependency on ax-13 2234 as well. See bj-ralvw 32059. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-rababwv 32061*	A weak version of rabab 3196 not using df-clel 2606 nor df-v 3175 (but requiring ax-ext 2590). A version without dv condition is provable by replacing bj-vexwv 32051 with bj-vexw 32049 in the proof, hence requiring ax-13 2234. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ {𝑥 ∈ {𝑦 ∣ 𝜓} ∣ 𝜑} = {𝑥 ∣ 𝜑}
Theorem	bj-ralcom4 32062*	Remove from ralcom4 3197 dependency on ax-ext 2590 and ax-13 2234 (and on df-or 384, df-an 385, df-tru 1478, df-sb 1868, df-clab 2597, df-cleq 2603, df-clel 2606, df-nfc 2740, df-v 3175). This proof uses only df-ral 2901 on top of first-order logic. (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑)
Theorem	bj-rexcom4 32063*	Remove from rexcom4 3198 dependency on ax-ext 2590 and ax-13 2234 (and on df-or 384, df-tru 1478, df-sb 1868, df-clab 2597, df-cleq 2603, df-clel 2606, df-nfc 2740, df-v 3175). This proof uses only df-rex 2902 on top of first-order logic. (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
Theorem	bj-rexcom4a 32064*	Remove from rexcom4a 3199 dependency on ax-ext 2590 and ax-13 2234 (and on df-or 384, df-sb 1868, df-clab 2597, df-cleq 2603, df-clel 2606, df-nfc 2740, df-v 3175). This proof uses only df-rex 2902 on top of first-order logic. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ ∃𝑥𝜓))
Theorem	bj-rexcom4bv 32065*	Version of bj-rexcom4b 32066 with a dv condition on 𝑥, 𝑉, hence removing dependency on df-sb 1868 and df-clab 2597 (so that it depends on df-clel 2606 and df-rex 2902 only on top of first-order logic). Prefer its use over bj-rexcom4b 32066 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ 𝐵 ∈ 𝑉    ⇒   ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑)
Theorem	bj-rexcom4b 32066*	Remove from rexcom4b 3200 dependency on ax-ext 2590 and ax-13 2234 (and on df-or 384, df-cleq 2603, df-nfc 2740, df-v 3175). The hypothesis uses 𝑉 instead of V (see bj-isseti 32058 for the motivation). Use bj-rexcom4bv 32065 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝐵 ∈ 𝑉    ⇒   ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑)
Theorem	bj-ceqsalt0 32067	The FOL content of ceqsalt 3201. Lemma for bj-ceqsalt 32069 and bj-ceqsaltv 32070. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜃 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥𝜃) → (∀𝑥(𝜃 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalt1 32068	The FOL content of ceqsalt 3201. Lemma for bj-ceqsalt 32069 and bj-ceqsaltv 32070. (TODO: consider removing if it does not add anything to bj-ceqsalt0 32067.) (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
⊢ (𝜃 → ∃𝑥𝜒)    ⇒   ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜒 → (𝜑 ↔ 𝜓)) ∧ 𝜃) → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalt 32069*	Remove from ceqsalt 3201 dependency on ax-ext 2590 (and on df-cleq 2603 and df-v 3175). Note: this is not doable with ceqsralt 3202 (or ceqsralv 3207), which uses eleq1 2676, but the same dependence removal is possible for ceqsalg 3203, ceqsal 3205, ceqsalv 3206, cgsexg 3211, cgsex2g 3212, cgsex4g 3213, ceqsex 3214, ceqsexv 3215, ceqsex2 3217, ceqsex2v 3218, ceqsex3v 3219, ceqsex4v 3220, ceqsex6v 3221, ceqsex8v 3222, gencbvex 3223 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3224, gencbval 3225, vtoclgft 3227 (it uses Ⅎ, whose justification nfcjust 2739 is actually provable without ax-ext 2590, as bj-nfcjust 32044 shows) and several other vtocl* theorems (see for instance bj-vtoclg1f 32103). See also bj-ceqsaltv 32070. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsaltv 32070*	Version of bj-ceqsalt 32069 with a dv condition on 𝑥, 𝑉, removing dependency on df-sb 1868 and df-clab 2597. Prefer its use over bj-ceqsalt 32069 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalg0 32071	The FOL content of ceqsalg 3203. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜒 → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalg 32072*	Remove from ceqsalg 3203 dependency on ax-ext 2590 (and on df-cleq 2603 and df-v 3175). See also bj-ceqsalgv 32074. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgALT 32073*	Alternate proof of bj-ceqsalg 32072. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgv 32074*	Version of bj-ceqsalg 32072 with a dv condition on 𝑥, 𝑉, removing dependency on df-sb 1868 and df-clab 2597. Prefer its use over bj-ceqsalg 32072 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgvALT 32075*	Alternate proof of bj-ceqsalgv 32074. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsal 32076*	Remove from ceqsal 3205 dependency on ax-ext 2590 (and on df-cleq 2603, df-v 3175, df-clab 2597, df-sb 1868). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	bj-ceqsalv 32077*	Remove from ceqsalv 3206 dependency on ax-ext 2590 (and on df-cleq 2603, df-v 3175, df-clab 2597, df-sb 1868). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	bj-spcimdv 32078*	Remove from spcimdv 3263 dependency on ax-10 2006, ax-11 2021, ax-13 2234, ax-ext 2590, df-cleq 2603 (and df-nfc 2740, df-v 3175, df-tru 1478, df-nf 1701). (Contributed by BJ, 30-Nov-2020.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
21.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 32079	The class-form not-free predicate defines a symmetric binary relation on var metavariables (irreflexivity is proved by nfnid 4823 with additional axioms; see also nfcv 2751). This could be proved from aecom 2299 and nfcvb 4824 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 2616 instead of equcomd 1933; removing dependency on ax-ext 2590 is possible: prove weak versions (i.e. replace classes with setvars) of drnfc1 2768, eleq2d 2673 (using elequ2 1991), nfcvf 2774, dvelimc 2773, dvelimdc 2772, nfcvf2 2775. (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝑦 ↔ Ⅎ𝑦𝑥)
21.14.5.4  Proposal for the definitions of class membership and class equality In this section, we show (bj-ax8 32080 and bj-ax9 32083) that the current forms of the definitions of class membership (df-clel 2606) and class equality (df-cleq 2603) are too powerful, and we propose alternate definitions (bj-df-clel 32081 and bj-df-cleq 32085) which also have the advantage of making it clear that these definitions are conservative.
Theorem	bj-ax8 32080	Proof of ax-8 1979 from df-clel 2606 (and FOL). This shows that df-clel 2606 is "too powerful". A possible definition is given by bj-df-clel 32081. (Contributed by BJ, 27-Jun-2019.) Also a direct consequence of bj-eleq1w 32040, which has essentially the same proof. (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
Theorem	bj-df-clel 32081*	Candidate definition for df-clel 2606 (the need for it is exposed in bj-ax8 32080). 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 32082, which should be used instead. The proof is irrelevant since this is a proposal for an axiom. Note: the current definition df-clel 2606 already mentions cleljust 1985 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.)
⊢ (𝑢 ∈ 𝑣 ↔ ∃𝑤(𝑤 = 𝑢 ∧ 𝑤 ∈ 𝑣))    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
Theorem	bj-dfclel 32082*	Characterization of the elements of a class. Note: cleljust 1985 could be relabeled as clelhyp. (Contributed by BJ, 27-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))
Theorem	bj-ax9 32083*	Proof of ax-9 1986 from ax-ext 2590 and df-cleq 2603 (and FOL) (with two extra dv conditions on 𝑥, 𝑧 and 𝑦, 𝑧). This shows that df-cleq 2603 is "too powerful". A possible definition is given by bj-df-cleq 32085. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
Theorem	bj-cleqhyp 32084*	The hypothesis of bj-df-cleq 32085. Note that the hypothesis of bj-df-cleq 32085 actually has an additional dv condition on 𝑥, 𝑦 and therefore is provable by simply using ax-ext 2590 in place of axext3 2592 in the current proof. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
Theorem	bj-df-cleq 32085*	Candidate definition for df-cleq 2603 (the need for it is exposed in bj-ax9 32083). 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 32086, 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.)
⊢ (𝑢 = 𝑣 ↔ ∀𝑤(𝑤 ∈ 𝑢 ↔ 𝑤 ∈ 𝑣))    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
Theorem	bj-dfcleq 32086*	Proof of class extensionality from the axiom of set extensionality (ax-ext 2590) and the definition of class equality (bj-df-cleq 32085). (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
21.14.5.5  Lemmas for class substitution Some useful theorems for dealing with substitutions: sbbi 2389, sbcbig 3447, sbcel1g 3939, sbcel2 3941, sbcel12 3935, sbceqg 3936, csbvarg 3955.
Theorem	bj-sbeqALT 32087*	Substitution in an equality (use the more genereal version bj-sbeq 32088 instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵)
Theorem	bj-sbeq 32088	Distribute proper substitution through an equality relation. (See sbceqg 3936). (Contributed by BJ, 6-Oct-2018.)
⊢ ([𝑦 / 𝑥]𝐴 = 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑦 / 𝑥⦌𝐵)
Theorem	bj-sbceqgALT 32089	Distribute proper substitution through an equality relation. Alternate proof of sbceqg 3936. (Contributed by BJ, 6-Oct-2018.) Proof modification is discouraged to avoid using sbceqg 3936, but "minimize */except sbceqg" is ok. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶))
Theorem	bj-csbsnlem 32090*	Lemma for bj-csbsn 32091 (in this lemma, 𝑥 cannot occur in 𝐴). (Contributed by BJ, 6-Oct-2018.) (New usage is discouraged.)
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴}
Theorem	bj-csbsn 32091	Substitution in a singleton. (Contributed by BJ, 6-Oct-2018.)
⊢ ⦋𝐴 / 𝑥⦌{𝑥} = {𝐴}
Theorem	bj-sbel1 32092*	Version of sbcel1g 3939 when substituting a set. (Note: one could have a corresponding version of sbcel12 3935 when substituting a set, but the point here is that the antecedent of sbcel1g 3939 is not needed when substituting a set.) (Contributed by BJ, 6-Oct-2018.)
⊢ ([𝑦 / 𝑥]𝐴 ∈ 𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ 𝐵)
Theorem	bj-abv 32093	The class of sets verifying a tautology is the universal class. (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → {𝑥 ∣ 𝜑} = V)
Theorem	bj-ab0 32094	The class of sets verifying a falsity is the empty set (closed form of abf 3930). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 ¬ 𝜑 → {𝑥 ∣ 𝜑} = ∅)
Theorem	bj-abf 32095	Shorter proof of abf 3930 (which should be kept as abfALT). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ ¬ 𝜑    ⇒   ⊢ {𝑥 ∣ 𝜑} = ∅
Theorem	bj-csbprc 32096	More direct proof of csbprc 3932 (fewer essential steps). (Contributed by BJ, 24-Jul-2019.) (Proof modification is discouraged.)
⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 = ∅)
21.14.5.6  Removing some dv conditions
Theorem	bj-exlimmpi 32097	Lemma for bj-vtoclg1f1 32102 (an instance of this lemma is a version of bj-vtoclg1f1 32102 where 𝑥 and 𝑦 are identified). (Contributed by BJ, 30-Apr-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 → 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpbi 32098	Lemma for theorems of the vtoclg 3239 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (∃𝑥𝜒 → 𝜓)
Theorem	bj-exlimmpbir 32099	Lemma for theorems of the vtoclg 3239 family. (Contributed by BJ, 3-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜓    ⇒   ⊢ (∃𝑥𝜒 → 𝜑)
Theorem	bj-vtoclf 32100*	Remove dependency on ax-ext 2590, df-clab 2597 and df-cleq 2603 (and df-sb 1868 and df-v 3175) from vtoclf 3231. (Contributed by BJ, 6-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ 𝑉    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓