P. 36 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 3501-3600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ceqsexv 3501*	Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) Avoid ax-12 2178. (Revised by GG, 12-Oct-2024.) (Proof shortened by Wolf Lammen, 22-Jan-2025.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)
Theorem	ceqsexv2d 3502*	Elimination of an existential quantifier, using implicit substitution. (Contributed by Thierry Arnoux, 10-Sep-2016.) Shorten, reduce dv conditions. (Revised by Wolf Lammen, 5-Jun-2025.) (Proof shortened by SN, 5-Jun-2025.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜓    ⇒   ⊢ ∃𝑥𝜑
Theorem	ceqsexv2dOLD 3503*	Obsolete version of ceqsexv2d 3502 as of 5-Jun-2025. (Contributed by Thierry Arnoux, 10-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜓    ⇒   ⊢ ∃𝑥𝜑
Theorem	ceqsex2 3504*	Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑) ↔ 𝜒)
Theorem	ceqsex2v 3505*	Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.) Avoid ax-10 2142 and ax-11 2158. (Revised by GG, 20-Aug-2023.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑) ↔ 𝜒)
Theorem	ceqsex3v 3506*	Elimination of three existential quantifiers, using implicit substitution. (Contributed by NM, 16-Aug-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜑) ↔ 𝜃)
Theorem	ceqsex4v 3507*	Elimination of four existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷) ∧ 𝜑) ↔ 𝜏)
Theorem	ceqsex6v 3508*	Elimination of six existential quantifiers, using implicit substitution. (Contributed by NM, 21-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐸 ∈ V    &   ⊢ 𝐹 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑣 = 𝐸 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑢 = 𝐹 → (𝜂 ↔ 𝜁))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ (𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑) ↔ 𝜁)
Theorem	ceqsex8v 3509*	Elimination of eight existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐸 ∈ V    &   ⊢ 𝐹 ∈ V    &   ⊢ 𝐺 ∈ V    &   ⊢ 𝐻 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑣 = 𝐸 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑢 = 𝐹 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑡 = 𝐺 → (𝜁 ↔ 𝜎))    &   ⊢ (𝑠 = 𝐻 → (𝜎 ↔ 𝜌))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤∃𝑣∃𝑢∃𝑡∃𝑠(((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ∧ ((𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ (𝑡 = 𝐺 ∧ 𝑠 = 𝐻)) ∧ 𝜑) ↔ 𝜌)
Theorem	gencbvex 3510*	Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ 𝐴 ∈ V    &   ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝑦))    ⇒   ⊢ (∃𝑥(𝜒 ∧ 𝜑) ↔ ∃𝑦(𝜃 ∧ 𝜓))
Theorem	gencbvex2 3511*	Restatement of gencbvex 3510 with weaker hypotheses. (Contributed by Jeff Hankins, 6-Dec-2006.)
⊢ 𝐴 ∈ V    &   ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜃 → ∃𝑥(𝜒 ∧ 𝐴 = 𝑦))    ⇒   ⊢ (∃𝑥(𝜒 ∧ 𝜑) ↔ ∃𝑦(𝜃 ∧ 𝜓))
Theorem	gencbval 3512*	Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.)
⊢ 𝐴 ∈ V    &   ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝑦))    ⇒   ⊢ (∀𝑥(𝜒 → 𝜑) ↔ ∀𝑦(𝜃 → 𝜓))
Theorem	sbhypf 3513*	Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf 3893. (Contributed by Raph Levien, 10-Apr-2004.) (Proof shortened by Wolf Lammen, 25-Jan-2025.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
Theorem	sbhypfOLD 3514*	Obsolete version of sbhypf 3513 as of 25-Jan-2025. (Contributed by Raph Levien, 10-Apr-2004.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
Theorem	spcimgft 3515	Closed theorem form of spcimgf 3519. (Contributed by Wolf Lammen, 28-Jul-2025.)
⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓))) → (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓)))
Theorem	spcimgfi1 3516	A closed version of spcimgf 3519. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 27-Jul-2025.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥𝜑 → 𝜓)))
Theorem	spcimgfi1OLD 3517	Obsolete version of spcimgfi1 3516 as of 27-Jul-2025. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥𝜑 → 𝜓)))
Theorem	spcgft 3518	A closed version of spcgf 3560. (Contributed by Andrew Salmon, 6-Jun-2011.) (Revised by Mario Carneiro, 4-Jan-2017.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥𝜑 → 𝜓)))
Theorem	spcimgf 3519	Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓))
Theorem	spcimegf 3520	Existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜓 → 𝜑))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))
Theorem	vtoclgft 3521	Closed theorem form of vtoclgf 3538. The reverse implication is proven in ceqsal1t 3483. See ceqsalt 3484 for a version with 𝑥 and 𝐴 disjoint. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by JJ, 11-Aug-2021.) Avoid ax-13 2371. (Revised by GG, 6-Oct-2023.)
⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → 𝜓)
Theorem	vtocleg 3522*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 21-Jun-1993.)
⊢ (𝑥 = 𝐴 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜑)
Theorem	vtoclg 3523*	Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.) Avoid ax-12 2178. (Revised by SN, 20-Apr-2024.) (Proof shortened by Wolf Lammen, 26-Jan-2025.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	vtocle 3524*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 9-Sep-1993.) Avoid df-clab 2709. (Revised by Wolf Lammen, 31-May-2025.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	vtocleOLD 3525*	Obsolete version of vtocle 3524 as of 31-May-2025. (Contributed by NM, 9-Sep-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	vtoclbg 3526*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))
Theorem	vtocl 3527*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2142. (Revised by BJ, 29-Nov-2020.) (Proof shortened by SN, 20-Apr-2024.) (Proof shortened by Wolf Lammen, 20-Jun-2025.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	vtoclOLD 3528*	Obsolete version of vtocl 3527 as of 20-Jun-2025. (Contributed by NM, 30-Aug-1993.) Remove dependency on ax-10 2142. (Revised by BJ, 29-Nov-2020.) (Proof shortened by SN, 20-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	vtocldf 3529	Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝜓)    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	vtocld 3530*	Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.) Avoid ax-10 2142, ax-11 2158, ax-12 2178. (Revised by SN, 2-Sep-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	vtocl2d 3531*	Implicit substitution of two classes for two setvar variables. (Contributed by Thierry Arnoux, 25-Aug-2020.) (Revised by BTernaryTau, 19-Oct-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	vtoclef 3532*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 18-Aug-1993.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	vtoclf 3533*	Implicit substitution of a class for a setvar variable. This is a generalization of chvar 2394. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 26-Jan-2025.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	vtoclfOLD 3534*	Obsolete version of vtoclf 3533 as of 26-Jan-2025. (Contributed by NM, 30-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	vtocl2 3535*	Implicit substitution of classes for setvar variables. (Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	vtocl3 3536*	Implicit substitution of classes for setvar variables. (Contributed by NM, 3-Jun-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Avoid ax-10 2142 and ax-11 2158. (Revised by GG, 20-Aug-2023.) (Proof shortened by Wolf Lammen, 23-Aug-2023.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	vtoclb 3537*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 23-Dec-1993.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜒 ↔ 𝜃)
Theorem	vtoclgf 3538	Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of disjoint variable restrictions. (Contributed by NM, 21-Sep-2003.) (Proof shortened by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	vtoclg1f 3539*	Version of vtoclgf 3538 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-10 2142 and ax-11 2158. (Contributed by BJ, 1-May-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	vtoclgOLD 3540*	Obsolete version of vtoclg 3523 as of 26-Jan-2025. (Contributed by NM, 17-Apr-1995.) Avoid ax-12 2178. (Revised by SN, 20-Apr-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	vtocl2gf 3541	Implicit substitution of a class for a setvar variable. (Contributed by NM, 25-Apr-1995.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ 𝜑    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒)
Theorem	vtocl3gf 3542	Implicit substitution of a class for a setvar variable. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑧𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ Ⅎ𝑧𝜃    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ 𝜑    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝜃)
Theorem	vtocl2g 3543*	Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.) Remove dependency on ax-10 2142, ax-11 2158, and ax-13 2371. (Revised by Steven Nguyen, 29-Nov-2022.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ 𝜑    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒)
Theorem	vtocl3g 3544*	Implicit substitution of a class for a setvar variable. Version of vtocl3gf 3542 with disjoint variable conditions instead of nonfreeness hypotheses, requiring fewer axioms. (Contributed by GG, 3-Oct-2024.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ 𝜑    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝜃)
Theorem	vtoclgaf 3545*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 17-Feb-2006.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ 𝐵 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝐵 → 𝜓)
Theorem	vtoclga 3546*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2142 and ax-11 2158. (Revised by GG, 20-Aug-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ 𝐵 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝐵 → 𝜓)
Theorem	vtocl2ga 3547*	Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2142 and ax-11 2158. (Revised by GG, 20-Aug-2023.) (Proof shortened by Wolf Lammen, 23-Aug-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒)
Theorem	vtocl2gaf 3548*	Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 10-Aug-2013.) (Proof shortened by Wolf Lammen, 31-May-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒)
Theorem	vtocl2gafOLD 3549*	Obsolete version of vtocl2gaf 3548 as of 31-May-2025. (Contributed by NM, 10-Aug-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒)
Theorem	vtocl3gaf 3550*	Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 11-Oct-2016.) (Proof shortened by Wolf Lammen, 31-May-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑧𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ Ⅎ𝑧𝜃    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → 𝜃)
Theorem	vtocl3gafOLD 3551*	Obsolete version of vtocl3gaf 3550 as of 31-May-2025. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 11-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑧𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ Ⅎ𝑧𝜃    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → 𝜃)
Theorem	vtocl3ga 3552*	Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 20-Aug-1995.) Reduce axiom usage. (Revised by GG, 3-Oct-2024.) (Proof shortened by Wolf Lammen, 31-May-2025.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑆) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑆) → 𝜃)
Theorem	vtocl3gaOLD 3553*	Obsolete version of vtocl3ga 3552 as of 31-May-2025. (Contributed by NM, 20-Aug-1995.) Reduce axiom usage. (Revised by GG, 3-Oct-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑆) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑆) → 𝜃)
Theorem	vtocl4g 3554*	Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜌))    &   ⊢ (𝑤 = 𝐷 → (𝜌 ↔ 𝜃))    &   ⊢ 𝜑    ⇒   ⊢ (((𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇)) → 𝜃)
Theorem	vtocl4ga 3555*	Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019.) (Proof shortened by Wolf Lammen, 31-May-2025.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜌))    &   ⊢ (𝑤 = 𝐷 → (𝜌 ↔ 𝜃))    &   ⊢ (((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑅) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇)) → 𝜑)    ⇒   ⊢ (((𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇)) → 𝜃)
Theorem	vtocl4gaOLD 3556*	Obsolete version of vtocl4ga 3555 as of 31-May-2025. (Contributed by AV, 22-Jan-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜌))    &   ⊢ (𝑤 = 𝐷 → (𝜌 ↔ 𝜃))    &   ⊢ (((𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑅) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇)) → 𝜑)    ⇒   ⊢ (((𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇)) → 𝜃)
Theorem	vtoclegft 3557*	Implicit substitution of a class for a setvar variable. (Closed theorem version of vtoclef 3532.) (Contributed by NM, 7-Nov-2005.) (Revised by Mario Carneiro, 11-Oct-2016.) (Proof shortened by Wolf Lammen, 26-Jan-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ Ⅎ𝑥𝜑 ∧ ∀𝑥(𝑥 = 𝐴 → 𝜑)) → 𝜑)
Theorem	vtoclegftOLD 3558*	Obsolete version of vtoclegft 3557 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 3559*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 21-Nov-1994.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ∀𝑥 ∈ 𝐵 𝜑    ⇒   ⊢ (𝐴 ∈ 𝐵 → 𝜓)
Theorem	spcgf 3560	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 3561	Existential specialization, using implicit substitution. (Contributed by NM, 2-Feb-1997.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))
Theorem	spcimdv 3562*	Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.) Avoid ax-10 2142 and ax-11 2158. (Revised by GG, 20-Aug-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	spcdv 3563*	Rule of specialization, using implicit substitution. Analogous to rspcdv 3583. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	spcimedv 3564*	Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → (𝜒 → ∃𝑥𝜓))
Theorem	spcgv 3565*	Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.) Avoid ax-10 2142, ax-11 2158. (Revised by Wolf Lammen, 25-Aug-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓))
Theorem	spcegv 3566*	Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) Avoid ax-10 2142, ax-11 2158. (Revised by Wolf Lammen, 25-Aug-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))
Theorem	spcedv 3567*	Existential specialization, using implicit substitution, deduction version. (Contributed by RP, 12-Aug-2020.) (Revised by AV, 16-Aug-2024.)
⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	spc2egv 3568*	Existential specialization with two quantifiers, using implicit substitution. (Contributed by NM, 3-Aug-1995.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝜓 → ∃𝑥∃𝑦𝜑))
Theorem	spc2gv 3569*	Specialization with two quantifiers, using implicit substitution. (Contributed by NM, 27-Apr-2004.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥∀𝑦𝜑 → 𝜓))
Theorem	spc2ed 3570*	Existential specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017.)
⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (𝜒 → ∃𝑥∃𝑦𝜓))
Theorem	spc2d 3571*	Specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017.)
⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊)) → (∀𝑥∀𝑦𝜓 → 𝜒))
Theorem	spc3egv 3572*	Existential specialization with three quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.) Avoid ax-10 2142 and ax-11 2158. (Revised by GG, 20-Aug-2023.) (Proof shortened by Wolf Lammen, 25-Aug-2023.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝜓 → ∃𝑥∃𝑦∃𝑧𝜑))
Theorem	spc3gv 3573*	Specialization with three quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀𝑥∀𝑦∀𝑧𝜑 → 𝜓))
Theorem	spcv 3574*	Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spcev 3575*	Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜓 → ∃𝑥𝜑)
Theorem	spc2ev 3576*	Existential specialization, using implicit substitution. (Contributed by NM, 3-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜓 → ∃𝑥∃𝑦𝜑)
Theorem	rspct 3577*	A closed version of rspc 3579. (Contributed by Andrew Salmon, 6-Jun-2011.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)))
Theorem	rspcdf 3578*	Restricted specialization, using implicit substitution. (Contributed by Emmett Weisz, 16-Jan-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝜒    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))
Theorem	rspc 3579*	Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
Theorem	rspce 3580*	Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) (Revised by Mario Carneiro, 11-Oct-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)
Theorem	rspcimdv 3581*	Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))
Theorem	rspcimedv 3582*	Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓))
Theorem	rspcdv 3583*	Restricted specialization, using implicit substitution. (Contributed by NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))
Theorem	rspcedv 3584*	Restricted existential specialization, using implicit substitution. (Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓))
Theorem	rspcebdv 3585*	Restricted existential specialization, using implicit substitution in both directions. (Contributed by AV, 8-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑥 = 𝐴)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ 𝜒))
Theorem	rspcdv2 3586*	Restricted specialization, using implicit substitution. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	rspcv 3587*	Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2142, ax-11 2158, ax-12 2178. (Revised by SN, 12-Dec-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
Theorem	rspccv 3588*	Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓))
Theorem	rspcva 3589*	Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)
Theorem	rspccva 3590*	Restricted specialization, using implicit substitution. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓)
Theorem	rspcev 3591*	Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) Drop ax-10 2142, ax-11 2158, ax-12 2178. (Revised by SN, 12-Dec-2023.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)
Theorem	rspcdva 3592*	Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ (𝑥 = 𝐶 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	rspcedvd 3593*	Restricted existential specialization, using implicit substitution. Variant of rspcedv 3584. (Contributed by AV, 27-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
Theorem	rspcedvdw 3594*	Version of rspcedvd 3593 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 3595*	Restricted existential specialization, using implicit substitution in both directions. (Contributed by Zhi Wang, 28-Sep-2024.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝜓 → 𝜒))    &   ⊢ ((𝜑 ∧ 𝜒) → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ 𝜒))
Theorem	rspcime 3596*	Prove a restricted existential. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
Theorem	rspceaimv 3597*	Restricted existential specialization of a universally quantified implication. (Contributed by BJ, 24-Aug-2022.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒))
Theorem	rspcedeq1vd 3598*	Restricted existential specialization, using implicit substitution. Variant of rspcedvd 3593 for equations, in which the left hand side depends on the quantified variable. (Contributed by AV, 24-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐶 = 𝐷)
Theorem	rspcedeq2vd 3599*	Restricted existential specialization, using implicit substitution. Variant of rspcedvd 3593 for equations, in which the right hand side depends on the quantified variable. (Contributed by AV, 24-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐶 = 𝐷)
Theorem	rspc2 3600*	Restricted specialization with two quantifiers, using implicit substitution. (Contributed by NM, 9-Nov-2012.)
⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))