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