P. 37 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 3601-3700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	vtoclegft 3601*	Implicit substitution of a class for a setvar variable. (Closed theorem version of vtoclef 3575.) (Contributed by NM, 7-Nov-2005.) (Revised by Mario Carneiro, 11-Oct-2016.) (Proof shortened by Wolf Lammen, 26-Jan-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ Ⅎ𝑥𝜑 ∧ ∀𝑥(𝑥 = 𝐴 → 𝜑)) → 𝜑)
Theorem	vtoclegftOLD 3602*	Obsolete version of vtoclegft 3601 as of 26-Jan-2025. (Contributed by NM, 7-Nov-2005.) (Revised by Mario Carneiro, 11-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝐵 ∧ Ⅎ𝑥𝜑 ∧ ∀𝑥(𝑥 = 𝐴 → 𝜑)) → 𝜑)
Theorem	vtoclri 3603*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 21-Nov-1994.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ∀𝑥 ∈ 𝐵 𝜑    ⇒   ⊢ (𝐴 ∈ 𝐵 → 𝜓)
Theorem	spcgf 3604	Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 2-Feb-1997.) (Revised by Andrew Salmon, 12-Aug-2011.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓))
Theorem	spcegf 3605	Existential specialization, using implicit substitution. (Contributed by NM, 2-Feb-1997.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))
Theorem	spcimdv 3606*	Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.) Avoid ax-10 2141 and ax-11 2158. (Revised by GG, 20-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	spcdv 3607*	Rule of specialization, using implicit substitution. Analogous to rspcdv 3627. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	spcimedv 3608*	Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → (𝜒 → ∃𝑥𝜓))
Theorem	spcgv 3609*	Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.) Avoid ax-10 2141, ax-11 2158. (Revised by Wolf Lammen, 25-Aug-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓))
Theorem	spcegv 3610*	Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) Avoid ax-10 2141, ax-11 2158. (Revised by Wolf Lammen, 25-Aug-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))
Theorem	spcedv 3611*	Existential specialization, using implicit substitution, deduction version. (Contributed by RP, 12-Aug-2020.) (Revised by AV, 16-Aug-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	spc2egv 3612*	Existential specialization with two quantifiers, using implicit substitution. (Contributed by NM, 3-Aug-1995.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝜓 → ∃𝑥∃𝑦𝜑))
Theorem	spc2gv 3613*	Specialization with two quantifiers, using implicit substitution. (Contributed by NM, 27-Apr-2004.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥∀𝑦𝜑 → 𝜓))
Theorem	spc2ed 3614*	Existential specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017.)
⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (𝜒 → ∃𝑥∃𝑦𝜓))
Theorem	spc2d 3615*	Specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017.)
⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∀𝑥∀𝑦𝜓 → 𝜒))
Theorem	spc3egv 3616*	Existential specialization with three quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.) Avoid ax-10 2141 and ax-11 2158. (Revised by GG, 20-Aug-2023.) (Proof shortened by Wolf Lammen, 25-Aug-2023.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝜓 → ∃𝑥∃𝑦∃𝑧𝜑))
Theorem	spc3gv 3617*	Specialization with three quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀𝑥∀𝑦∀𝑧𝜑 → 𝜓))
Theorem	spcv 3618*	Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spcev 3619*	Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜓 → ∃𝑥𝜑)
Theorem	spc2ev 3620*	Existential specialization, using implicit substitution. (Contributed by NM, 3-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜓 → ∃𝑥∃𝑦𝜑)
Theorem	rspct 3621*	A closed version of rspc 3623. (Contributed by Andrew Salmon, 6-Jun-2011.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)))
Theorem	rspcdf 3622*	Restricted specialization, using implicit substitution. (Contributed by Emmett Weisz, 16-Jan-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))
Theorem	rspc 3623*	Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
Theorem	rspce 3624*	Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) (Revised by Mario Carneiro, 11-Oct-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)
Theorem	rspcimdv 3625*	Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))
Theorem	rspcimedv 3626*	Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓))
Theorem	rspcdv 3627*	Restricted specialization, using implicit substitution. (Contributed by NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))
Theorem	rspcedv 3628*	Restricted existential specialization, using implicit substitution. (Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓))
Theorem	rspcebdv 3629*	Restricted existential specialization, using implicit substitution in both directions. (Contributed by AV, 8-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑥 = 𝐴)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ 𝜒))
Theorem	rspcdv2 3630*	Restricted specialization, using implicit substitution. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	rspcv 3631*	Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2141, ax-11 2158, ax-12 2178. (Revised by SN, 12-Dec-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
Theorem	rspccv 3632*	Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓))
Theorem	rspcva 3633*	Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)
Theorem	rspccva 3634*	Restricted specialization, using implicit substitution. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓)
Theorem	rspcev 3635*	Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2141, ax-11 2158, ax-12 2178. (Revised by SN, 12-Dec-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)
Theorem	rspcdva 3636*	Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ (𝑥 = 𝐶 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	rspcedvd 3637*	Restricted existential specialization, using implicit substitution. Variant of rspcedv 3628. (Contributed by AV, 27-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
Theorem	rspcedvdw 3638*	Version of rspcedvd 3637 where the implicit substitution hypothesis does not have an antecedent, which also avoids a disjoint variable condition on 𝜑, 𝑥. (Contributed by SN, 20-Aug-2024.)
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
Theorem	rspceb2dv 3639*	Restricted existential specialization, using implicit substitution in both directions. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝜓 → 𝜒))    &   ⊢ ((𝜑 ∧ 𝜒) → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ 𝜒))
Theorem	rspcime 3640*	Prove a restricted existential. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
Theorem	rspceaimv 3641*	Restricted existential specialization of a universally quantified implication. (Contributed by BJ, 24-Aug-2022.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒))
Theorem	rspcedeq1vd 3642*	Restricted existential specialization, using implicit substitution. Variant of rspcedvd 3637 for equations, in which the left hand side depends on the quantified variable. (Contributed by AV, 24-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐶 = 𝐷)
Theorem	rspcedeq2vd 3643*	Restricted existential specialization, using implicit substitution. Variant of rspcedvd 3637 for equations, in which the right hand side depends on the quantified variable. (Contributed by AV, 24-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐶 = 𝐷)
Theorem	rspc2 3644*	Restricted specialization with two quantifiers, using implicit substitution. (Contributed by NM, 9-Nov-2012.)
⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))
Theorem	rspc2gv 3645*	Restricted specialization with two quantifiers, using implicit substitution. (Contributed by BJ, 2-Dec-2021.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 𝜑 → 𝜓))
Theorem	rspc2v 3646*	2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))
Theorem	rspc2va 3647*	2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓)
Theorem	rspc2ev 3648*	2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)
Theorem	2rspcedvdw 3649*	Double application of rspcedvdw 3638. (Contributed by SN, 24-Aug-2024.)
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 𝜓)
Theorem	rspc2dv 3650*	2-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 6-Mar-2025.)
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑦 = 𝐵 → (𝜃 ↔ 𝜒))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐶)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐷)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	rspc3v 3651*	3-variable restricted specialization, using implicit substitution. (Contributed by NM, 10-May-2005.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓))
Theorem	rspc3ev 3652*	3-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 25-Jul-2012.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓))    ⇒   ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑇 𝜑)
Theorem	3rspcedvdw 3653*	Triple application of rspcedvdw 3638. (Contributed by SN, 20-Aug-2024.)
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜏))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑍)    &   ⊢ (𝜑 → 𝜏)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ∃𝑧 ∈ 𝑍 𝜓)
Theorem	rspc3dv 3654*	3-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2025.)
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑦 = 𝐵 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑧 = 𝐶 → (𝜏 ↔ 𝜒))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧 ∈ 𝐹 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐸)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐹)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	rspc4v 3655*	4-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 7-Feb-2025.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑤 = 𝐷 → (𝜏 ↔ 𝜓))    ⇒   ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈)) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 ∀𝑤 ∈ 𝑈 𝜑 → 𝜓))
Theorem	rspc6v 3656*	6-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 20-Feb-2025.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑤 = 𝐷 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑝 = 𝐸 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑞 = 𝐹 → (𝜁 ↔ 𝜓))    ⇒   ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈) ∧ (𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊)) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 ∀𝑤 ∈ 𝑈 ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 𝜑 → 𝜓))
Theorem	rspc8v 3657*	8-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 20-Feb-2025.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑤 = 𝐷 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑝 = 𝐸 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑞 = 𝐹 → (𝜁 ↔ 𝜎))    &   ⊢ (𝑟 = 𝐺 → (𝜎 ↔ 𝜌))    &   ⊢ (𝑠 = 𝐻 → (𝜌 ↔ 𝜓))    ⇒   ⊢ ((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈)) ∧ ((𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) ∧ (𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌))) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 ∀𝑤 ∈ 𝑈 ∀𝑝 ∈ 𝑉 ∀𝑞 ∈ 𝑊 ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 𝜑 → 𝜓))
Theorem	rspceeqv 3658*	Restricted existential specialization in an equality, using implicit substitution. (Contributed by BJ, 2-Sep-2022.)
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐸 = 𝐷) → ∃𝑥 ∈ 𝐵 𝐸 = 𝐶)
Theorem	ralxpxfr2d 3659*	Transfer a universal quantifier between one variable with pair-like semantics and two. (Contributed by Stefan O'Rear, 27-Feb-2015.)
⊢ 𝐴 ∈ V    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 ∃𝑧 ∈ 𝐷 𝑥 = 𝐴))    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐷 𝜒))
Theorem	rexraleqim 3660*	Statement following from existence and generalization with equality. (Contributed by AV, 9-Feb-2019.)
⊢ (𝑥 = 𝑧 → (𝜓 ↔ 𝜑))    &   ⊢ (𝑧 = 𝑌 → (𝜑 ↔ 𝜃))    ⇒   ⊢ ((∃𝑧 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝑥 = 𝑌)) → 𝜃)
Theorem	eqvincg 3661*	A variable introduction law for class equality, closed form. (Contributed by Thierry Arnoux, 2-Mar-2017.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵)))
Theorem	eqvinc 3662*	A variable introduction law for class equality. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Proof shortened by Thierry Arnoux, 23-Jan-2022.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵))
Theorem	eqvincf 3663	A variable introduction law for class equality, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 14-Sep-2003.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵))
Theorem	alexeqg 3664*	Two ways to express substitution of 𝐴 for 𝑥 in 𝜑. This is the analogue for classes of sbalex 2243. (Contributed by NM, 2-Mar-1995.) (Revised by BJ, 27-Apr-2019.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)))
Theorem	ceqex 3665*	Equality implies equivalence with substitution. (Contributed by NM, 2-Mar-1995.) (Proof shortened by BJ, 1-May-2019.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)))
Theorem	ceqsexg 3666*	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 11-Oct-2004.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓))
Theorem	ceqsexgv 3667*	Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 29-Dec-1996.) Drop ax-10 2141 and ax-12 2178. (Revised by GG, 1-Dec-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓))
Theorem	ceqsrexv 3668*	Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 30-Apr-2004.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓))
Theorem	ceqsrexbv 3669*	Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
Theorem	ceqsralbv 3670*	Elimination of a restricted universal quantifier, using implicit substitution. (Contributed by Scott Fenton, 7-Dec-2020.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))
Theorem	ceqsrex2v 3671*	Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 29-Oct-2005.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝜑) ↔ 𝜒))
Theorem	clel2g 3672*	Alternate definition of membership when the member is a set. (Contributed by NM, 18-Aug-1993.) Strengthen from sethood hypothesis to sethood antecedent. (Revised by BJ, 12-Feb-2022.) Avoid ax-12 2178. (Revised by BJ, 1-Sep-2024.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)))
Theorem	clel2 3673*	Alternate definition of membership when the member is a set. (Contributed by NM, 18-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
Theorem	clel3g 3674*	Alternate definition of membership in a set. (Contributed by NM, 13-Aug-2005.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥)))
Theorem	clel3 3675*	Alternate definition of membership in a set. (Contributed by NM, 18-Aug-1993.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥))
Theorem	clel4g 3676*	Alternate definition of membership in a set. (Contributed by NM, 18-Aug-1993.) Strengthen from sethood hypothesis to sethood antecedent and avoid ax-12 2178. (Revised by BJ, 1-Sep-2024.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐵 → 𝐴 ∈ 𝑥)))
Theorem	clel4 3677*	Alternate definition of membership in a set. (Contributed by NM, 18-Aug-1993.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐵 → 𝐴 ∈ 𝑥))
Theorem	clel5 3678*	Alternate definition of class membership: a class 𝑋 is an element of another class 𝐴 iff there is an element of 𝐴 equal to 𝑋. (Contributed by AV, 13-Nov-2020.) Remove use of ax-10 2141, ax-11 2158, and ax-12 2178. (Revised by Steven Nguyen, 19-May-2023.)
⊢ (𝑋 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑋 = 𝑥)
Theorem	pm13.183 3679*	Compare theorem *13.183 in [WhiteheadRussell] p. 178. Only 𝐴 is required to be a set. (Contributed by Andrew Salmon, 3-Jun-2011.) Avoid ax-13 2380. (Revised by Wolf Lammen, 29-Apr-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 ↔ ∀𝑧(𝑧 = 𝐴 ↔ 𝑧 = 𝐵)))
Theorem	rr19.3v 3680*	Restricted quantifier version of Theorem 19.3 of [Margaris] p. 89. We don't need the nonempty class condition of r19.3rzv 4522 when there is an outer quantifier. (Contributed by NM, 25-Oct-2012.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rr19.28v 3681*	Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. We don't need the nonempty class condition of r19.28zv 4524 when there is an outer quantifier. (Contributed by NM, 29-Oct-2012.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓))
Theorem	elab6g 3682*	Membership in a class abstraction. Class version of sb6 2085. (Contributed by SN, 5-Oct-2024.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))
Theorem	elabd2 3683*	Membership in a class abstraction, using implicit substitution. Deduction version of elab 3694. (Contributed by GG, 12-Oct-2024.) (Revised by BJ, 16-Oct-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 = {𝑥 ∣ 𝜓})    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝜒))
Theorem	elabd3 3684*	Membership in a class abstraction, using implicit substitution. Deduction version of elab 3694. (Contributed by GG, 12-Oct-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝜒))
Theorem	elabgt 3685*	Membership in a class abstraction, using implicit substitution. (Closed theorem version of elabg 3690.) (Contributed by NM, 7-Nov-2005.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom usage. (Revised by GG, 12-Oct-2024.) (Proof shortend by Wolf Lammen, 11-May-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
Theorem	elabgtOLD 3686*	Obsolete version of elabgt 3685 as of 11-May-2025. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom usage. (Revised by GG, 12-Oct-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
Theorem	elabgtOLDOLD 3687*	Obsolete version of elabgt 3685 as of 12-Oct-2024. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
Theorem	elabgf 3688	Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) (Revised by Mario Carneiro, 12-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
Theorem	elabf 3689*	Membership in a class abstraction, using implicit substitution. (Contributed by NM, 1-Aug-1994.) (Revised by Mario Carneiro, 12-Oct-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)
Theorem	elabg 3690*	Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 14-Apr-1995.) Avoid ax-13 2380. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2141, ax-11 2158, ax-12 2178. (Revised by SN, 5-Oct-2024.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
Theorem	elabgOLD 3691*	Obsolete version of elabg 3690 as of 5-Oct-2024. (Contributed by NM, 14-Apr-1995.) Remove dependency on ax-13 2380. (Revised by SN, 23-Nov-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
Theorem	elabgw 3692*	Membership in a class abstraction, using two substitution hypotheses to avoid a disjoint variable condition on 𝑥 and 𝐴. This is to elabg 3690 what sbievw2 2098 is to sbievw 2093. (Contributed by SN, 20-Apr-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜒))
Theorem	elab2gw 3693*	Membership in a class abstraction, using two substitution hypotheses to avoid a disjoint variable condition on 𝑥 and 𝐴, which is not usually significant since 𝐵 is usually a constant. (Contributed by SN, 16-May-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒))    &   ⊢ 𝐵 = {𝑥 ∣ 𝜑}    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜒))
Theorem	elab 3694*	Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 1-Aug-1994.) Avoid ax-10 2141, ax-11 2158, ax-12 2178. (Revised by SN, 5-Oct-2024.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)
Theorem	elabOLD 3695*	Obsolete version of elab 3694 as of 5-Oct-2024. (Contributed by NM, 1-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)
Theorem	elab2g 3696*	Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝐵 = {𝑥 ∣ 𝜑}    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓))
Theorem	elabd 3697*	Explicit demonstration the class {𝑥 ∣ 𝜓} is not empty by the example 𝐴. (Contributed by RP, 12-Aug-2020.) (Revised by AV, 23-Mar-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∣ 𝜓})
Theorem	elab2 3698*	Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝐵 = {𝑥 ∣ 𝜑}    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ 𝜓)
Theorem	elab4g 3699*	Membership in a class abstraction, using implicit substitution. (Contributed by NM, 17-Oct-2012.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝐵 = {𝑥 ∣ 𝜑}    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ (𝐴 ∈ V ∧ 𝜓))
Theorem	elab3gf 3700	Membership in a class abstraction, with a weaker antecedent than elabgf 3688. (Contributed by NM, 6-Sep-2011.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝜓 → 𝐴 ∈ 𝐵) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))