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-stdpc5t 36801	Alias of bj-nnf-alrim 36788 for labeling consistency (a standard predicate calculus axiom). Closed form of stdpc5 2211 proved from modalK (obsoleting stdpc5v 1939). (Contributed by BJ, 2-Dec-2023.) Use bj-nnf-alrim 36788 instead. (New usaged is discouraged.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-19.21t 36802	Statement 19.21t 2209 proved from modalK (obsoleting 19.21v 1940). (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	bj-19.23t 36803	Statement 19.23t 2213 proved from modalK (obsoleting 19.23v 1943). (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)))
Theorem	bj-19.36im 36804	One direction of 19.36 2233 from the same axioms as 19.36imv 1946. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)))
Theorem	bj-19.37im 36805	One direction of 19.37 2235 from the same axioms as 19.37imv 1948. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓)))
Theorem	bj-19.42t 36806	Closed form of 19.42 2239 from the same axioms as 19.42v 1954. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)))
Theorem	bj-19.41t 36807	Closed form of 19.41 2238 from the same axioms as 19.41v 1950. The same is doable with 19.27 2230, 19.28 2231, 19.31 2237, 19.32 2236, 19.44 2240, 19.45 2241. (Contributed by BJ, 2-Dec-2023.)
⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)))
Theorem	bj-sbft 36808	Version of sbft 2272 using Ⅎ', proved from core axioms. (Contributed by BJ, 19-Nov-2023.)
⊢ (Ⅎ'𝑥𝜑 → ([𝑡 / 𝑥]𝜑 ↔ 𝜑))
Theorem	bj-pm11.53vw 36809	Version of pm11.53v 1945 with nonfreeness antecedents. One can also prove the theorem with antecedent (Ⅎ'𝑦∀𝑥𝜑 ∧ ∀𝑦Ⅎ'𝑥𝜓). (Contributed by BJ, 7-Oct-2024.)
⊢ ((∀𝑥Ⅎ'𝑦𝜑 ∧ Ⅎ'𝑥∀𝑦𝜓) → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-pm11.53v 36810	Version of pm11.53v 1945 with nonfreeness antecedents. (Contributed by BJ, 7-Oct-2024.)
⊢ ((∀𝑥Ⅎ'𝑦𝜑 ∧ ∀𝑦Ⅎ'𝑥𝜓) → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-pm11.53a 36811*	A variant of pm11.53v 1945. One can similarly prove a variant with DV (𝑦, 𝜑) and ∀𝑦Ⅎ'𝑥𝜓 instead of DV (𝑥, 𝜓) and ∀𝑥Ⅎ'𝑦𝜑. (Contributed by BJ, 7-Oct-2024.)
⊢ (∀𝑥Ⅎ'𝑦𝜑 → (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-equsvt 36812*	A variant of equsv 2004. (Contributed by BJ, 7-Oct-2024.)
⊢ (Ⅎ'𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑))
Theorem	bj-equsalvwd 36813*	Variant of equsalvw 2005. (Contributed by BJ, 7-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜒))
Theorem	bj-equsexvwd 36814*	Variant of equsexvw 2006. (Contributed by BJ, 7-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜒))
Theorem	bj-sbievwd 36815*	Variant of sbievw 2096. (Contributed by BJ, 7-Oct-2024.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → Ⅎ'𝑥𝜒)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))
21.19.4.11  Adding ax-13
Theorem	bj-axc10 36816	Alternate proof of axc10 2385. Shorter. One can prove a version with DV (𝑥, 𝑦) without ax-13 2372, by using ax6ev 1970 instead of ax6e 2383. (Contributed by BJ, 31-Mar-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Theorem	bj-alequex 36817	A fol lemma. See alequexv 2002 for a version with a disjoint variable condition requiring fewer axioms. Can be used to reduce the proof of spimt 2386 from 133 to 112 bytes. (Contributed by BJ, 6-Oct-2018.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
Theorem	bj-spimt2 36818	A step in the proof of spimt 2386. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∃𝑥𝜓 → 𝜓) → (∀𝑥𝜑 → 𝜓)))
Theorem	bj-cbv3ta 36819	Closed form of cbv3 2397. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦(∃𝑥𝜓 → 𝜓) ∧ ∀𝑥(𝜑 → ∀𝑦𝜑)) → (∀𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-cbv3tb 36820	Closed form of cbv3 2397. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥∀𝑦(𝑥 = 𝑦 → (𝜑 → 𝜓)) → ((∀𝑦Ⅎ𝑥𝜓 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∀𝑥𝜑 → ∀𝑦𝜓)))
Theorem	bj-hbsb3t 36821	A theorem close to a closed form of hbsb3 2487. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑))
Theorem	bj-hbsb3 36822	Shorter proof of hbsb3 2487. (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1t 36823	A theorem close to a closed form of nfs1 2488. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥(𝜑 → ∀𝑦𝜑) → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1t2 36824	A theorem close to a closed form of nfs1 2488. (Contributed by BJ, 2-May-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1 36825	Shorter proof of nfs1 2488 (three essential steps instead of four). (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
21.19.4.12  Removing dependencies on ax-13 (and ax-11) It is known that ax-13 2372 is logically redundant (see ax13w 2139 and the head comment of the section "Logical redundancy of ax-10--13"). More precisely, one can remove dependency on ax-13 2372 from every theorem in set.mm which is totally unbundled (i.e., has disjoint variable conditions on all setvar variables). Indeed, start with the existing proof, and replace any occurrence of ax-13 2372 with ax13w 2139. This section is an experiment to see in practice if (partially) unbundled versions of existing theorems can be proved more efficiently without ax-13 2372 (and using ax6v 1969 / ax6ev 1970 instead of ax-6 1968 / ax6e 2383, as is currently done). One reason to be optimistic is that the first few utility theorems using ax-13 2372 (roughly 200 of them) are then used mainly with dummy variables, which one can assume distinct from any other, so that the unbundled versions of the utility theorems suffice. In this section, we prove versions of theorems in the main part with dv conditions and not requiring ax-13 2372, labeled bj-xxxv (we follow the proof of xxx but use ax6v 1969 and ax6ev 1970 instead of ax-6 1968 and ax6e 2383, and ax-5 1911 instead of ax13v 2373; shorter proofs may be possible). When no additional dv condition is required, we label it bj-xxx. It is important to keep all the bundled theorems already in set.mm, but one may also add the (partially) unbundled versions which dispense with ax-13 2372, so as to remove dependencies on ax-13 2372 from many existing theorems. UPDATE: it turns out that several theorems of the form bj-xxxv, or minor variations, are already in set.mm with label xxxw. It is also possible to remove dependencies on ax-11 2160, typically by replacing a nonfree hypothesis with a disjoint variable condition (see cbv3v2 2244 and following theorems).
Theorem	bj-axc10v 36826*	Version of axc10 2385 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Theorem	bj-spimtv 36827*	Version of spimt 2386 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-cbv3hv2 36828*	Version of cbv3h 2404 with two disjoint variable conditions, which does not require ax-11 2160 nor ax-13 2372. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	bj-cbv1hv 36829*	Version of cbv1h 2405 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒)))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒))
Theorem	bj-cbv2hv 36830*	Version of cbv2h 2406 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbv2v 36831*	Version of cbv2 2403 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvaldv 36832*	Version of cbvald 2407 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvexdv 36833*	Version of cbvexd 2408 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	bj-cbval2vv 36834*	Version of cbval2vv 2413 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	bj-cbvex2vv 36835*	Version of cbvex2vv 2414 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	bj-cbvaldvav 36836*	Version of cbvaldva 2409 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvexdvav 36837*	Version of cbvexdva 2410 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	bj-cbvex4vv 36838*	Version of cbvex4v 2415 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒)
Theorem	bj-equsalhv 36839*	Version of equsalh 2420 with a disjoint variable condition, which does not require ax-13 2372. Remark: this is the same as equsalhw 2293. TODO: delete after moving the following paragraph somewhere. Remarks: equsexvw 2006 has been moved to Main; Theorem ax13lem2 2376 has a DV version which is a simple consequence of ax5e 1913; Theorems nfeqf2 2377, dveeq2 2378, nfeqf1 2379, dveeq1 2380, nfeqf 2381, axc9 2382, ax13 2375, have dv versions which are simple consequences of ax-5 1911. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	bj-axc11nv 36840*	Version of axc11n 2426 with a disjoint variable condition; instance of aevlem 2058. TODO: delete after checking surrounding theorems. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	bj-aecomsv 36841*	Version of aecoms 2428 with a disjoint variable condition, provable from Tarski's FOL. The corresponding version of naecoms 2429 should not be very useful since ¬ ∀𝑥𝑥 = 𝑦, DV (𝑥, 𝑦) is true when the universe has at least two objects (see dtru 5379). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	bj-axc11v 36842*	Version of axc11 2430 with a disjoint variable condition, which does not require ax-13 2372 nor ax-10 2144. Remark: the following theorems (hbae 2431, nfae 2433, hbnae 2432, nfnae 2434, hbnaes 2435) would need to be totally unbundled to be proved without ax-13 2372, hence would be simple consequences of ax-5 1911 or nfv 1915. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	bj-drnf2v 36843*	Version of drnf2 2444 with a disjoint variable condition, which does not require ax-10 2144, ax-11 2160, ax-12 2180, ax-13 2372. Instance of nfbidv 1923. Note that the version of axc15 2422 with a disjoint variable condition is actually ax12v2 2182 (up to adding a superfluous antecedent). (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓))
Theorem	bj-equs45fv 36844*	Version of equs45f 2459 with a disjoint variable condition, which does not require ax-13 2372. Note that the version of equs5 2460 with a disjoint variable condition is actually sbalex 2245 (up to adding a superfluous antecedent). (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	bj-hbs1 36845*	Version of hbsb2 2482 with a disjoint variable condition, which does not require ax-13 2372, and removal of ax-13 2372 from hbs1 2276. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1v 36846*	Version of nfsb2 2483 with a disjoint variable condition, which does not require ax-13 2372, and removal of ax-13 2372 from nfs1v 2159. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	bj-hbsb2av 36847*	Version of hbsb2a 2484 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-hbsb3v 36848*	Version of hbsb3 2487 with a disjoint variable condition, which does not require ax-13 2372. (Remark: the unbundled version of nfs1 2488 is given by bj-nfs1v 36846.) (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfsab1 36849*	Remove dependency on ax-13 2372 from nfsab1 2717. UPDATE / TODO: nfsab1 2717 does not use ax-13 2372 either anymore; bj-nfsab1 36849 is shorter than nfsab1 2717 but uses ax-12 2180. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	bj-dtrucor2v 36850*	Version of dtrucor2 5310 with a disjoint variable condition, which does not require ax-13 2372 (nor ax-4 1810, ax-5 1911, ax-7 2009, ax-12 2180). (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 36851	Biconditional version of a form of hbae 2431 with commuted quantifiers, not requiring ax-11 2160. (Contributed by BJ, 12-Dec-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑧 𝑥 = 𝑦)
Theorem	bj-hbaeb 36852	Biconditional version of hbae 2431. (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	bj-hbnaeb 36853	Biconditional version of hbnae 2432 (to replace it?). (Contributed by BJ, 6-Oct-2018.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	bj-dvv 36854	A special instance of bj-hbaeb2 36851. 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 36623), then they should be added to the database. The present case is similar. Similar additions can be done regarding equsex 2418 (and equsalh 2420 and equsexh 2421). Even if only one of these two theorems holds, it should be added to the database.
Theorem	bj-equsal1t 36855	Duplication of wl-equsal1t 37575, with shorter proof. If one imposes a disjoint variable condition on x,y , then one can use alequexv 2002 and reduce axiom dependencies, and similarly for the following theorems. Note: wl-equsalcom 37576 is also interesting. (Contributed by BJ, 6-Oct-2018.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑))
Theorem	bj-equsal1ti 36856	Inference associated with bj-equsal1t 36855. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)
Theorem	bj-equsal1 36857	One direction of equsal 2417. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜓)
Theorem	bj-equsal2 36858	One direction of equsal 2417. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓))
Theorem	bj-equsal 36859	Shorter proof of equsal 2417. (Contributed by BJ, 30-Sep-2018.) Proof modification is discouraged to avoid using equsal 2417, 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 36860	Closed form of stdpc5 2211. (Possible to place it before 19.21t 2209 and use it to prove 19.21t 2209). (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-stdpc5 36861	More direct proof of stdpc5 2211. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
Theorem	2stdpc5 36862	A double stdpc5 2211 (one direction of PM*11.3). See also 2stdpc4 2073 and 19.21vv 44408. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	bj-19.21t0 36863	Proof of 19.21t 2209 from stdpc5t 36860. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	exlimii 36864	Inference associated with exlimi 2220. Inferring a theorem when it is implied by an antecedent which may be true. (Contributed by BJ, 15-Sep-2018.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → 𝜓)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜓
Theorem	ax11-pm 36865	Proof of ax-11 2160 similar to PM's proof of alcom 2162 (PM*11.2). For a proof closer to PM's proof, see ax11-pm2 36869. Axiom ax-11 2160 is used in the proof only through nfa2 2179. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	ax6er 36866	Commuted form of ax6e 2383. (Could be placed right after ax6e 2383). (Contributed by BJ, 15-Sep-2018.)
⊢ ∃𝑥 𝑦 = 𝑥
Theorem	exlimiieq1 36867	Inferring a theorem when it is implied by an equality which may be true. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	exlimiieq2 36868	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 36869*	Proof of ax-11 2160 from the standard axioms of predicate calculus, similar to PM's proof of alcom 2162 (PM*11.2). This proof requires that 𝑥 and 𝑦 be distinct. Axiom ax-11 2160 is used in the proof only through nfal 2324, nfsb 2523, sbal 2172, sb8 2517. See also ax11-pm 36865. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
21.19.4.16  Alternate definition of substitution
Theorem	bj-sbsb 36870	Biconditional showing two possible (dual) definitions of substitution df-sb 2068 not using dummy variables. (Contributed by BJ, 19-Mar-2021.)
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))
Theorem	bj-dfsb2 36871	Alternate (dual) definition of substitution df-sb 2068 not using dummy variables. (Contributed by BJ, 19-Mar-2021.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))
21.19.4.17  Lemmas for substitution
Theorem	bj-sbf3 36872	Substitution has no effect on a bound variable (existential quantifier case); see sbf2 2274. (Contributed by BJ, 2-May-2019.)
⊢ ([𝑦 / 𝑥]∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-sbf4 36873	Substitution has no effect on a bound variable (nonfreeness case); see sbf2 2274. (Contributed by BJ, 2-May-2019.)
⊢ ([𝑦 / 𝑥]Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜑)
21.19.4.18  Existential uniqueness
Theorem	bj-eu3f 36874*	Version of eu3v 2565 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 2565. (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 36875*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜒)))
Theorem	bj-sblem2 36876*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝜑 → (𝜒 → 𝜓)) → ((∃𝑥𝜑 → 𝜒) → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-sblem 36877*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝜑 → (𝜓 ↔ 𝜒)) → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜒)))
Theorem	bj-sbievw1 36878*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → 𝜓))
Theorem	bj-sbievw2 36879*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ ([𝑦 / 𝑥](𝜓 → 𝜑) → (𝜓 → [𝑦 / 𝑥]𝜑))
Theorem	bj-sbievw 36880*	Lemma for substitution. Closed form of equsalvw 2005 and sbievw 2096. (Contributed by BJ, 23-Jul-2023.)
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
Theorem	bj-sbievv 36881	Version of sbie 2502 with a second nonfreeness hypothesis and shorter proof. (Contributed by BJ, 18-Jul-2023.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
Theorem	bj-moeub 36882	Uniqueness is equivalent to existence being equivalent to unique existence. (Contributed by BJ, 14-Oct-2022.)
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 ↔ ∃!𝑥𝜑))
Theorem	bj-sbidmOLD 36883	Obsolete proof of sbidm 2510 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 36884*	Deduction form of dvelim 2451 with disjoint variable conditions. Uncurried (imported) form of bj-dvelimdv1 36885. 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 1915 can be replaced with nfal 2324 followed by nfn 1858. Remark: nfald 2329 uses ax-11 2160; it might be possible to inline and use ax11w 2133 instead, but there is still a use via 19.12 2328 anyway. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜓))    ⇒   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)
Theorem	bj-dvelimdv1 36885*	Curried (exported) form of bj-dvelimdv 36884 (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 36886*	A version of dvelim 2451 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑧 = 𝑦 → (𝜓 ↔ 𝜑))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)
Theorem	bj-nfeel2 36887*	Nonfreeness in a membership statement. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 ∈ 𝑧)
Theorem	bj-axc14nf 36888	Proof of a version of axc14 2463 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧 𝑥 ∈ 𝑦))
Theorem	bj-axc14 36889	Alternate proof of axc14 2463 (even when inlining the above results, this gives a shorter proof). (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Theorem	mobidvALT 36890*	Alternate proof of mobidv 2544 directly from its analogues albidv 1921 and exbidv 1922, using deduction style. Note the proof structure, similar to mobi 2542. (Contributed by Mario Carneiro, 7-Oct-2016.) Reduce axiom dependencies and shorten proof. Remove dependency on ax-6 1968, ax-7 2009, ax-12 2180 by adapting proof of mobid 2545. (Revised by BJ, 26-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Theorem	sbn1ALT 36891	Alternate proof of sbn1 2110, 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 2703, df-clab 2710, df-cleq 2723, df-clel 2806 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 2703, df-clab 2710, df-cleq 2723, df-clel 2806 }) 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 36899, eliminable-abeqv 36900, eliminable-abeqab 36901, eliminable-velab 36898, eliminable-abelv 36902, eliminable-abelab 36903 respectively, which are all proved from {FOL, ax-ext 2703, df-clab 2710, df-cleq 2723, df-clel 2806 }. (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 2710, dfcleq 2724 (proved from {FOL, ax-ext 2703, df-cleq 2723 }), and dfclel 2807 (proved from {FOL, df-clel 2806 }). 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 36893, eliminable2b 36894 and eliminable3a 36896, 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 1540, 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 2710 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 2710, ax-ext 2703 and df-cleq 2723 are sufficient (over FOL) to eliminate class terms. To prove that { df-clab 2710, df-cleq 2723, df-clel 2806 } provides a definitional extension of {FOL, ax-ext 2703 }, 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 2710, df-cleq 2723, df-clel 2806 }. 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 2703 }. 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 2710, df-cleq 2723, df-clel 2806 }. It involves a careful case study on the structure of the proof tree.
Theorem	eliminable1 36892	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 36893*	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 36894*	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 36895*	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 36896*	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 36897*	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 36898	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 36899*	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 36900*	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.)
⊢ ({𝑥 ∣ 𝜑} = 𝑦 ↔ ∀𝑧([𝑧 / 𝑥]𝜑 ↔ 𝑧 ∈ 𝑦))