P. 372 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37101-37200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bj-spimtv 37101*	Version of spimt 2390 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓))
Theorem	bj-cbv3hv2 37102*	Version of cbv3h 2408 with two disjoint variable conditions, which does not require ax-11 2163 nor ax-13 2376. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	bj-cbv1hv 37103*	Version of cbv1h 2409 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒)))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒))
Theorem	bj-cbv2hv 37104*	Version of cbv2h 2410 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbv2v 37105*	Version of cbv2 2407 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvaldv 37106*	Version of cbvald 2411 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvexdv 37107*	Version of cbvexd 2412 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	bj-cbval2vv 37108*	Version of cbval2vv 2417 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	bj-cbvex2vv 37109*	Version of cbvex2vv 2418 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	bj-cbvaldvav 37110*	Version of cbvaldva 2413 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	bj-cbvexdvav 37111*	Version of cbvexdva 2414 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	bj-cbvex4vv 37112*	Version of cbvex4v 2419 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒)
Theorem	bj-equsalhv 37113*	Version of equsalh 2424 with a disjoint variable condition, which does not require ax-13 2376. Remark: this is the same as equsalhw 2298. TODO: delete after moving the following paragraph somewhere. Remarks: equsexvw 2007 has been moved to Main; Theorem ax13lem2 2380 has a DV version which is a simple consequence of ax5e 1914; Theorems nfeqf2 2381, dveeq2 2382, nfeqf1 2383, dveeq1 2384, nfeqf 2385, axc9 2386, ax13 2379, have dv versions which are simple consequences of ax-5 1912. (Contributed by BJ, 14-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	bj-axc11nv 37114*	Version of axc11n 2430 with a disjoint variable condition; instance of aevlem 2059. TODO: delete after checking surrounding theorems. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	bj-aecomsv 37115*	Version of aecoms 2432 with a disjoint variable condition, provable from Tarski's FOL. The corresponding version of naecoms 2433 should not be very useful since ¬ ∀𝑥𝑥 = 𝑦, DV (𝑥, 𝑦) is true when the universe has at least two objects (see dtru 5389). (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	bj-axc11v 37116*	Version of axc11 2434 with a disjoint variable condition, which does not require ax-13 2376 nor ax-10 2147. Remark: the following theorems (hbae 2435, nfae 2437, hbnae 2436, nfnae 2438, hbnaes 2439) would need to be totally unbundled to be proved without ax-13 2376, hence would be simple consequences of ax-5 1912 or nfv 1916. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	bj-drnf2v 37117*	Version of drnf2 2448 with a disjoint variable condition, which does not require ax-10 2147, ax-11 2163, ax-12 2185, ax-13 2376. Instance of nfbidv 1924. Note that the version of axc15 2426 with a disjoint variable condition is actually ax12v2 2187 (up to adding a superfluous antecedent). (Contributed by BJ, 17-Jun-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓))
Theorem	bj-equs45fv 37118*	Version of equs45f 2463 with a disjoint variable condition, which does not require ax-13 2376. Note that the version of equs5 2464 with a disjoint variable condition is actually sbalex 2250 (up to adding a superfluous antecedent). (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	bj-hbs1 37119*	Version of hbsb2 2486 with a disjoint variable condition, which does not require ax-13 2376, and removal of ax-13 2376 from hbs1 2281. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfs1v 37120*	Version of nfsb2 2487 with a disjoint variable condition, which does not require ax-13 2376, and removal of ax-13 2376 from nfs1v 2162. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	bj-hbsb2av 37121*	Version of hbsb2a 2488 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-hbsb3v 37122*	Version of hbsb3 2491 with a disjoint variable condition, which does not require ax-13 2376. (Remark: the unbundled version of nfs1 2492 is given by bj-nfs1v 37120.) (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	bj-nfsab1 37123*	Remove dependency on ax-13 2376 from nfsab1 2722. UPDATE / TODO: nfsab1 2722 does not use ax-13 2376 either anymore; bj-nfsab1 37123 is shorter than nfsab1 2722 but uses ax-12 2185. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
Theorem	bj-dtrucor2v 37124*	Version of dtrucor2 5314 with a disjoint variable condition, which does not require ax-13 2376 (nor ax-4 1811, ax-5 1912, ax-7 2010, ax-12 2185). (Contributed by BJ, 16-Jul-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → 𝑥 ≠ 𝑦)    ⇒   ⊢ (𝜑 ∧ ¬ 𝜑)
21.19.4.15  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 37125	Biconditional version of a form of hbae 2435 with commuted quantifiers, not requiring ax-11 2163. (Contributed by BJ, 12-Dec-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥∀𝑧 𝑥 = 𝑦)
Theorem	bj-hbaeb 37126	Biconditional version of hbae 2435. (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	bj-hbnaeb 37127	Biconditional version of hbnae 2436 (to replace it?). (Contributed by BJ, 6-Oct-2018.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	bj-dvv 37128	A special instance of bj-hbaeb2 37125. 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.16  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 36855), then they should be added to the database. The present case is similar. Similar additions can be done regarding equsex 2422 (and equsalh 2424 and equsexh 2425). Even if only one of these two theorems holds, it should be added to the database.
Theorem	bj-equsal1t 37129	Duplication of wl-equsal1t 37867, with shorter proof. If one imposes a disjoint variable condition on 𝑥, 𝑦, then one can use alequexv 2003 and reduce axiom dependencies, and similarly for the following theorems. Note: wl-equsalcom 37868 is also interesting. (Contributed by BJ, 6-Oct-2018.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑))
Theorem	bj-equsal1ti 37130	Inference associated with bj-equsal1t 37129. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)
Theorem	bj-equsal1 37131	One direction of equsal 2421. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜓)
Theorem	bj-equsal2 37132	One direction of equsal 2421. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓))
Theorem	bj-equsal 37133	Shorter proof of equsal 2421. (Contributed by BJ, 30-Sep-2018.) Proof modification is discouraged to avoid using equsal 2421, but "min */exc equsal" is ok. (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
21.19.4.17  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 37134	Closed form of stdpc5 2216. (Possible to place it before 19.21t 2214 and use it to prove 19.21t 2214). (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)))
Theorem	bj-stdpc5 37135	More direct proof of stdpc5 2216. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))
Theorem	2stdpc5 37136	A double stdpc5 2216 (one direction of PM*11.3). See also 2stdpc4 2076 and 19.21vv 44803. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → (𝜑 → ∀𝑥∀𝑦𝜓))
Theorem	bj-19.21t0 37137	Proof of 19.21t 2214 from stdpc5t 37134. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)))
Theorem	exlimii 37138	Inference associated with exlimi 2225. Inferring a theorem when it is implied by an antecedent which may be true. (Contributed by BJ, 15-Sep-2018.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → 𝜓)    &   ⊢ ∃𝑥𝜑    ⇒   ⊢ 𝜓
Theorem	ax11-pm 37139	Proof of ax-11 2163 similar to PM's proof of alcom 2165 (PM*11.2). For a proof closer to PM's proof, see ax11-pm2 37143. Axiom ax-11 2163 is used in the proof only through nfa2 2182. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	ax6er 37140	Commuted form of ax6e 2387. (Could be placed right after ax6e 2387). (Contributed by BJ, 15-Sep-2018.)
⊢ ∃𝑥 𝑦 = 𝑥
Theorem	exlimiieq1 37141	Inferring a theorem when it is implied by an equality which may be true. (Contributed by BJ, 30-Sep-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	exlimiieq2 37142	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 37143*	Proof of ax-11 2163 from the standard axioms of predicate calculus, similar to PM's proof of alcom 2165 (PM*11.2). This proof requires that 𝑥 and 𝑦 be distinct. Axiom ax-11 2163 is used in the proof only through nfal 2328, nfsb 2527, sbal 2175, sb8 2521. See also ax11-pm 37139. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
21.19.4.18  Alternate definition of substitution
Theorem	bj-sbsb 37144	Biconditional showing two possible (dual) definitions of substitution df-sb 2069 not using dummy variables. (Contributed by BJ, 19-Mar-2021.)
⊢ (((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))
Theorem	bj-dfsb2 37145	Alternate (dual) definition of substitution df-sb 2069 not using dummy variables. (Contributed by BJ, 19-Mar-2021.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ∨ (𝑥 = 𝑦 ∧ 𝜑)))
21.19.4.19  Lemmas for substitution
Theorem	bj-sbf3 37146	Substitution has no effect on a bound variable (existential quantifier case); see sbf2 2279. (Contributed by BJ, 2-May-2019.)
⊢ ([𝑦 / 𝑥]∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-sbf4 37147	Substitution has no effect on a bound variable (nonfreeness case); see sbf2 2279. (Contributed by BJ, 2-May-2019.)
⊢ ([𝑦 / 𝑥]Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜑)
21.19.4.20  Existential uniqueness
Theorem	bj-eu3f 37148*	Version of eu3v 2570 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 2570. (Contributed by NM, 8-Jul-1994.) (Proof shortened by BJ, 31-May-2019.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
21.19.4.21  First-order logic: miscellaneous Miscellaneous theorems of first-order logic.
Theorem	bj-sblem1 37149*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → 𝜒)))
Theorem	bj-sblem2 37150*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝜑 → (𝜒 → 𝜓)) → ((∃𝑥𝜑 → 𝜒) → ∀𝑥(𝜑 → 𝜓)))
Theorem	bj-sblem 37151*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ (∀𝑥(𝜑 → (𝜓 ↔ 𝜒)) → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜒)))
Theorem	bj-sbievw1 37152*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → 𝜓))
Theorem	bj-sbievw2 37153*	Lemma for substitution. (Contributed by BJ, 23-Jul-2023.)
⊢ ([𝑦 / 𝑥](𝜓 → 𝜑) → (𝜓 → [𝑦 / 𝑥]𝜑))
Theorem	bj-sbievw 37154*	Lemma for substitution. Closed form of equsalvw 2006 and sbievw 2099. (Contributed by BJ, 23-Jul-2023.)
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
Theorem	bj-sbievv 37155	Version of sbie 2506 with a second nonfreeness hypothesis and shorter proof. (Contributed by BJ, 18-Jul-2023.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
Theorem	bj-moeub 37156	Uniqueness is equivalent to existence being equivalent to unique existence. (Contributed by BJ, 14-Oct-2022.)
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 ↔ ∃!𝑥𝜑))
Theorem	bj-sbidmOLD 37157	Obsolete proof of sbidm 2514 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 37158*	Deduction form of dvelim 2455 with disjoint variable conditions. Uncurried (imported) form of bj-dvelimdv1 37159. 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 1916 can be replaced with nfal 2328 followed by nfn 1859. Remark: nfald 2333 uses ax-11 2163; it might be possible to inline and use ax11w 2136 instead, but there is still a use via 19.12 2332 anyway. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝑧 = 𝑦 → (𝜒 ↔ 𝜓))    ⇒   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)
Theorem	bj-dvelimdv1 37159*	Curried (exported) form of bj-dvelimdv 37158 (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 37160*	A version of dvelim 2455 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑧 = 𝑦 → (𝜓 ↔ 𝜑))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜑)
Theorem	bj-nfeel2 37161*	Nonfreeness in a membership statement. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 ∈ 𝑧)
Theorem	bj-axc14nf 37162	Proof of a version of axc14 2467 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧 𝑥 ∈ 𝑦))
Theorem	bj-axc14 37163	Alternate proof of axc14 2467 (even when inlining the above results, this gives a shorter proof). (Contributed by BJ, 20-Oct-2021.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Theorem	mobidvALT 37164*	Alternate proof of mobidv 2549 directly from its analogues albidv 1922 and exbidv 1923, using deduction style. Note the proof structure, similar to mobi 2547. (Contributed by Mario Carneiro, 7-Oct-2016.) Reduce axiom dependencies and shorten proof. Remove dependency on ax-12 2185 by adapting proof of mobid 2550. (Revised by BJ, 26-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Theorem	sbn1ALT 37165	Alternate proof of sbn1 2113, 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 2708, df-clab 2715, df-cleq 2728, df-clel 2811 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 2708, df-clab 2715, df-cleq 2728, df-clel 2811 }) 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 37173, eliminable-abeqv 37174, eliminable-abeqab 37175, eliminable-velab 37172, eliminable-abelv 37176, eliminable-abelab 37177 respectively, which are all proved from {FOL, ax-ext 2708, df-clab 2715, df-cleq 2728, df-clel 2811 }. (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 2715, dfcleq 2729 (proved from {FOL, ax-ext 2708, df-cleq 2728 }), and dfclel 2812 (proved from {FOL, df-clel 2811 }). 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 37167, eliminable2b 37168 and eliminable3a 37170, 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 1541, 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 2715 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 2715, ax-ext 2708 and df-cleq 2728 are sufficient (over FOL) to eliminate class terms. To prove that { df-clab 2715, df-cleq 2728, df-clel 2811 } provides a definitional extension of {FOL, ax-ext 2708 }, 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 2715, df-cleq 2728, df-clel 2811 }. 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 2708 }. 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 2715, df-cleq 2728, df-clel 2811 }. It involves a careful case study on the structure of the proof tree.
Theorem	eliminable1 37166	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 37167*	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 37168*	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 37169*	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 37170*	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 37171*	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 37172	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 37173*	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 37174*	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 37175*	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 37176*	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 37177*	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 2708. One could move all theorems from cab 2714 to df-clel 2811 (except for dfcleq 2729 and cvjust 2730) 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 2728. Note that without ax-ext 2708, the $a-statements df-clab 2715, df-cleq 2728, and df-clel 2811 are no longer eliminable (see previous section) (but PROBABLY df-clab 2715 is still conservative , while df-cleq 2728 and df-clel 2811 are not). This is not a reason not to study what is provable with them but without ax-ext 2708, 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 2114, wel 2115, ax-8 2116, ax-9 2124). Remark: the weakening of eleq1 2824 / eleq2 2825 to eleq1w 2819 / eleq2w 2820 can also be done with eleq1i 2827, eqeltri 2832, eqeltrri 2833, eleq1a 2831, eleq1d 2821, eqeltrd 2836, eqeltrrd 2837, eqneltrd 2856, eqneltrrd 2857, nelneq 2860. Remark: possibility to remove dependency on ax-10 2147, ax-11 2163, ax-13 2376 from nfcri 2890 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 2911.
Theorem	bj-denoteslem 37178*	Duplicate of issettru 2814 and bj-issettruALTV 37180. Lemma for bj-denotesALTV 37179. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-denotesALTV 37179*	Moved to main as iseqsetv-clel 2815 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 2039, and eqeq1 2740, requires the core axioms and { ax-9 2124, ax-ext 2708, df-cleq 2728 } whereas this proof requires the core axioms and { ax-8 2116, df-clab 2715, df-clel 2811 }. Theorem bj-issetwt 37182 proves that "existing" is equivalent to being a member of a class abstraction. It also requires, with the present proof, { ax-8 2116, df-clab 2715, df-clel 2811 } (whereas with the shorter proof from cbvexvw 2039 and eqeq1 2740 it would require { ax-8 2116, ax-9 2124, ax-ext 2708, df-clab 2715, df-cleq 2728, df-clel 2811 }). That every class is equal to a class abstraction is proved by abid1 2872, which requires { ax-8 2116, ax-9 2124, ax-ext 2708, df-clab 2715, df-cleq 2728, df-clel 2811 }. Note that there is no disjoint variable condition on 𝑥, 𝑦 but the theorem does not depend on ax-13 2376. Actually, the proof depends only on the logical axioms ax-1 6 through ax-7 2010 and sp 2191. 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 2708 and df-cleq 2728 (e.g., eqid 2736 and eqeq1 2740). In particular, one cannot even prove ⊢ ∃𝑥𝑥 = 𝐴 ⇒ ⊢ 𝐴 = 𝐴 without ax-ext 2708 and df-cleq 2728. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	bj-issettruALTV 37180*	Moved to main as issettru 2814 and kept for the comments. Weak version of isset 3443 without ax-ext 2708. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.)
⊢ (∃𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-elabtru 37181	This is as close as we can get to proving extensionality for "the" "universal" class without ax-ext 2708. (Contributed by BJ, 24-Apr-2024.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ {𝑥 ∣ ⊤} ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
Theorem	bj-issetwt 37182*	Closed form of bj-issetw 37183. (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴))
Theorem	bj-issetw 37183*	The closest one can get to isset 3443 without using ax-ext 2708. See also vexw 2720. Note that the only disjoint variable condition is between 𝑦 and 𝐴. From there, one can prove isset 3443 using eleq2i 2828 (which requires ax-ext 2708 and df-cleq 2728). (Contributed by BJ, 29-Apr-2019.) (Proof modification is discouraged.)
⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦 𝑦 = 𝐴)
Theorem	bj-issetiv 37184*	Version of bj-isseti 37185 with a disjoint variable condition on 𝑥, 𝑉. The hypothesis uses 𝑉 instead of V for extra generality. This is indeed more general than isseti 3447 as long as elex 3450 is not available (and the non-dependence of bj-issetiv 37184 on special properties of the universal class V is obvious). Prefer its use over bj-isseti 37185 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 14-Sep-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∃𝑥 𝑥 = 𝐴
Theorem	bj-isseti 37185*	Version of isseti 3447 with a class variable 𝑉 in the hypothesis instead of V for extra generality. This is indeed more general than isseti 3447 as long as elex 3450 is not available (and the non-dependence of bj-isseti 37185 on special properties of the universal class V is obvious). Use bj-issetiv 37184 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 13-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ 𝑉    ⇒   ⊢ ∃𝑥 𝑥 = 𝐴
Theorem	bj-ralvw 37186	A weak version of ralv 3456 not using ax-ext 2708 (nor df-cleq 2728, df-clel 2811, df-v 3431), and only core FOL axioms. See also bj-rexvw 37187. The analogues for reuv 3458 and rmov 3459 are not proved. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ (∀𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∀𝑥𝜑)
Theorem	bj-rexvw 37187	A weak version of rexv 3457 not using ax-ext 2708 (nor df-cleq 2728, df-clel 2811, df-v 3431), and only core FOL axioms. See also bj-ralvw 37186. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ (∃𝑥 ∈ {𝑦 ∣ 𝜓}𝜑 ↔ ∃𝑥𝜑)
Theorem	bj-rababw 37188	A weak version of rabab 3460 not using df-clel 2811 nor df-v 3431 (but requiring ax-ext 2708) nor ax-12 2185. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝜓    ⇒   ⊢ {𝑥 ∈ {𝑦 ∣ 𝜓} ∣ 𝜑} = {𝑥 ∣ 𝜑}
Theorem	bj-rexcom4bv 37189*	Version of rexcom4b 3461 and bj-rexcom4b 37190 with a disjoint variable condition on 𝑥, 𝑉, hence removing dependency on df-sb 2069 and df-clab 2715 (so that it depends on df-clel 2811 and df-rex 3062 only on top of first-order logic). Prefer its use over bj-rexcom4b 37190 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 37190*	Remove from rexcom4b 3461 dependency on ax-ext 2708 and ax-13 2376 (and on df-or 849, df-cleq 2728, df-nfc 2885, df-v 3431). The hypothesis uses 𝑉 instead of V (see bj-isseti 37185 for the motivation). Use bj-rexcom4bv 37189 instead when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ 𝐵 ∈ 𝑉    ⇒   ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑)
Theorem	bj-ceqsalt0 37191	The FOL content of ceqsalt 3463. Lemma for bj-ceqsalt 37193 and bj-ceqsaltv 37194. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜃 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥𝜃) → (∀𝑥(𝜃 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalt1 37192	The FOL content of ceqsalt 3463. Lemma for bj-ceqsalt 37193 and bj-ceqsaltv 37194. TODO: consider removing if it does not add anything to bj-ceqsalt0 37191. (Contributed by BJ, 26-Sep-2019.) (Proof modification is discouraged.)
⊢ (𝜃 → ∃𝑥𝜒)    ⇒   ⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝜒 → (𝜑 ↔ 𝜓)) ∧ 𝜃) → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalt 37193*	Remove from ceqsalt 3463 dependency on ax-ext 2708 (and on df-cleq 2728 and df-v 3431). Note: this is not doable with ceqsralt 3464 (or ceqsralv 3470), which uses eleq1 2824, but the same dependence removal is possible for ceqsalg 3465, ceqsal 3467, ceqsalv 3469, cgsexg 3474, cgsex2g 3475, cgsex4g 3476, ceqsex 3477, ceqsexv 3478, ceqsex2 3481, ceqsex2v 3482, ceqsex3v 3483, ceqsex4v 3484, ceqsex6v 3485, ceqsex8v 3486, gencbvex 3487 (after changing 𝐴 = 𝑦 to 𝑦 = 𝐴), gencbvex2 3488, gencbval 3489, vtoclgft 3497 (it uses Ⅎ, whose justification nfcjust 2884 does not use ax-ext 2708) and several other vtocl* theorems (see for instance bj-vtoclg1f 37225). See also bj-ceqsaltv 37194. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsaltv 37194*	Version of bj-ceqsalt 37193 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2069 and df-clab 2715. Prefer its use over bj-ceqsalt 37193 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalg0 37195	The FOL content of ceqsalg 3465. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜒 → (∀𝑥(𝜒 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalg 37196*	Remove from ceqsalg 3465 dependency on ax-ext 2708 (and on df-cleq 2728 and df-v 3431). See also bj-ceqsalgv 37198. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgALT 37197*	Alternate proof of bj-ceqsalg 37196. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgv 37198*	Version of bj-ceqsalg 37196 with a disjoint variable condition on 𝑥, 𝑉, removing dependency on df-sb 2069 and df-clab 2715. Prefer its use over bj-ceqsalg 37196 when sufficient (in particular when 𝑉 is substituted for V). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsalgvALT 37199*	Alternate proof of bj-ceqsalgv 37198. (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	bj-ceqsal 37200*	Remove from ceqsal 3467 dependency on ax-ext 2708 (and on df-cleq 2728, df-v 3431, df-clab 2715, df-sb 2069). (Contributed by BJ, 12-Oct-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)