P. 29 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2801-2900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ceqsex2v 2801*	Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑) ↔ 𝜒)
Theorem	ceqsex3v 2802*	Elimination of three existential quantifiers, using implicit substitution. (Contributed by NM, 16-Aug-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜑) ↔ 𝜃)
Theorem	ceqsex4v 2803*	Elimination of four existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷) ∧ 𝜑) ↔ 𝜏)
Theorem	ceqsex6v 2804*	Elimination of six existential quantifiers, using implicit substitution. (Contributed by NM, 21-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐸 ∈ V    &   ⊢ 𝐹 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑣 = 𝐸 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑢 = 𝐹 → (𝜂 ↔ 𝜁))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ (𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑) ↔ 𝜁)
Theorem	ceqsex8v 2805*	Elimination of eight existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐸 ∈ V    &   ⊢ 𝐹 ∈ V    &   ⊢ 𝐺 ∈ V    &   ⊢ 𝐻 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑣 = 𝐸 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑢 = 𝐹 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑡 = 𝐺 → (𝜁 ↔ 𝜎))    &   ⊢ (𝑠 = 𝐻 → (𝜎 ↔ 𝜌))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤∃𝑣∃𝑢∃𝑡∃𝑠(((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ∧ ((𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ (𝑡 = 𝐺 ∧ 𝑠 = 𝐻)) ∧ 𝜑) ↔ 𝜌)
Theorem	gencbvex 2806*	Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ 𝐴 ∈ V    &   ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝑦))    ⇒   ⊢ (∃𝑥(𝜒 ∧ 𝜑) ↔ ∃𝑦(𝜃 ∧ 𝜓))
Theorem	gencbvex2 2807*	Restatement of gencbvex 2806 with weaker hypotheses. (Contributed by Jeff Hankins, 6-Dec-2006.)
⊢ 𝐴 ∈ V    &   ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜃 → ∃𝑥(𝜒 ∧ 𝐴 = 𝑦))    ⇒   ⊢ (∃𝑥(𝜒 ∧ 𝜑) ↔ ∃𝑦(𝜃 ∧ 𝜓))
Theorem	gencbval 2808*	Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.) (Proof rewritten by Jim Kingdon, 20-Jun-2018.)
⊢ 𝐴 ∈ V    &   ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝑦))    ⇒   ⊢ (∀𝑥(𝜒 → 𝜑) ↔ ∀𝑦(𝜃 → 𝜓))
Theorem	sbhypf 2809*	Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf . (Contributed by Raph Levien, 10-Apr-2004.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
Theorem	vtoclgft 2810	Closed theorem form of vtoclgf 2818. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 12-Oct-2016.)
⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → 𝜓)
Theorem	vtocldf 2811	Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝜓)    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	vtocld 2812*	Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	vtoclf 2813*	Implicit substitution of a class for a setvar variable. This is a generalization of chvar 1768. (Contributed by NM, 30-Aug-1993.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	vtocl 2814*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	vtocl2 2815*	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 2816*	Implicit substitution of classes for setvar variables. (Contributed by NM, 3-Jun-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	vtoclb 2817*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 23-Dec-1993.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜒 ↔ 𝜃)
Theorem	vtoclgf 2818	Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) (Proof shortened by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	vtoclg1f 2819*	Version of vtoclgf 2818 with one nonfreeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-11 1517 and ax-13 2166. (Contributed by BJ, 1-May-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	vtoclg 2820*	Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	vtoclbg 2821*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))
Theorem	vtocl2gf 2822	Implicit substitution of a class for a setvar variable. (Contributed by NM, 25-Apr-1995.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ 𝜑    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒)
Theorem	vtocl3gf 2823	Implicit substitution of a class for a setvar variable. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑧𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ Ⅎ𝑧𝜃    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ 𝜑    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝜃)
Theorem	vtocl2g 2824*	Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ 𝜑    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒)
Theorem	vtoclgaf 2825*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 17-Feb-2006.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ 𝐵 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝐵 → 𝜓)
Theorem	vtoclga 2826*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ 𝐵 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝐵 → 𝜓)
Theorem	vtocl2gaf 2827*	Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 10-Aug-2013.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒)
Theorem	vtocl2ga 2828*	Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒)
Theorem	vtocl3gaf 2829*	Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 11-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑧𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ Ⅎ𝑧𝜃    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → 𝜃)
Theorem	vtocl3ga 2830*	Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 20-Aug-1995.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑆) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑆) → 𝜃)
Theorem	vtocleg 2831*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 10-Jan-2004.)
⊢ (𝑥 = 𝐴 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜑)
Theorem	vtoclegft 2832*	Implicit substitution of a class for a setvar variable. (Closed theorem version of vtoclef 2833.) (Contributed by NM, 7-Nov-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
⊢ ((𝐴 ∈ 𝐵 ∧ Ⅎ𝑥𝜑 ∧ ∀𝑥(𝑥 = 𝐴 → 𝜑)) → 𝜑)
Theorem	vtoclef 2833*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 18-Aug-1993.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	vtocle 2834*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 9-Sep-1993.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	vtoclri 2835*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 21-Nov-1994.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ∀𝑥 ∈ 𝐵 𝜑    ⇒   ⊢ (𝐴 ∈ 𝐵 → 𝜓)
Theorem	spcimgft 2836	A closed version of spcimgf 2840. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥𝜑 → 𝜓)))
Theorem	spcgft 2837	A closed version of spcgf 2842. (Contributed by Andrew Salmon, 6-Jun-2011.) (Revised by Mario Carneiro, 4-Jan-2017.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥𝜑 → 𝜓)))
Theorem	spcimegft 2838	A closed version of spcimegf 2841. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜓 → 𝜑)) → (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥𝜑)))
Theorem	spcegft 2839	A closed version of spcegf 2843. (Contributed by Jim Kingdon, 22-Jun-2018.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥𝜑)))
Theorem	spcimgf 2840	Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓))
Theorem	spcimegf 2841	Existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜓 → 𝜑))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))
Theorem	spcgf 2842	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 2843	Existential specialization, using implicit substitution. (Contributed by NM, 2-Feb-1997.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))
Theorem	spcimdv 2844*	Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	spcdv 2845*	Rule of specialization, using implicit substitution. Analogous to rspcdv 2867. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	spcimedv 2846*	Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → (𝜒 → ∃𝑥𝜓))
Theorem	spcgv 2847*	Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓))
Theorem	spcegv 2848*	Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))
Theorem	spcedv 2849*	Existential specialization, using implicit substitution, deduction version. (Contributed by RP, 12-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ V)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	spc2egv 2850*	Existential specialization with 2 quantifiers, using implicit substitution. (Contributed by NM, 3-Aug-1995.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝜓 → ∃𝑥∃𝑦𝜑))
Theorem	spc2gv 2851*	Specialization with 2 quantifiers, using implicit substitution. (Contributed by NM, 27-Apr-2004.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥∀𝑦𝜑 → 𝜓))
Theorem	spc3egv 2852*	Existential specialization with 3 quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝜓 → ∃𝑥∃𝑦∃𝑧𝜑))
Theorem	spc3gv 2853*	Specialization with 3 quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀𝑥∀𝑦∀𝑧𝜑 → 𝜓))
Theorem	spcv 2854*	Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spcev 2855*	Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜓 → ∃𝑥𝜑)
Theorem	spc2ev 2856*	Existential specialization, using implicit substitution. (Contributed by NM, 3-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜓 → ∃𝑥∃𝑦𝜑)
Theorem	rspct 2857*	A closed version of rspc 2858. (Contributed by Andrew Salmon, 6-Jun-2011.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)))
Theorem	rspc 2858*	Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
Theorem	rspce 2859*	Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) (Revised by Mario Carneiro, 11-Oct-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)
Theorem	rspcv 2860*	Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
Theorem	rspccv 2861*	Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓))
Theorem	rspcva 2862*	Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)
Theorem	rspccva 2863*	Restricted specialization, using implicit substitution. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓)
Theorem	rspcev 2864*	Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)
Theorem	rspcimdv 2865*	Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))
Theorem	rspcimedv 2866*	Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓))
Theorem	rspcdv 2867*	Restricted specialization, using implicit substitution. (Contributed by NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))
Theorem	rspcedv 2868*	Restricted existential specialization, using implicit substitution. (Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓))
Theorem	rspcdva 2869*	Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ (𝑥 = 𝐶 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	rspcedvd 2870*	Restricted existential specialization, using implicit substitution. Variant of rspcedv 2868. (Contributed by AV, 27-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
Theorem	rspcime 2871*	Prove a restricted existential. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
Theorem	rspceaimv 2872*	Restricted existential specialization of a universally quantified implication. (Contributed by BJ, 24-Aug-2022.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 (𝜓 → 𝜒)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 (𝜑 → 𝜒))
Theorem	rspcedeq1vd 2873*	Restricted existential specialization, using implicit substitution. Variant of rspcedvd 2870 for equations, in which the left hand side depends on the quantified variable. (Contributed by AV, 24-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐶 = 𝐷)
Theorem	rspcedeq2vd 2874*	Restricted existential specialization, using implicit substitution. Variant of rspcedvd 2870 for equations, in which the right hand side depends on the quantified variable. (Contributed by AV, 24-Dec-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐶 = 𝐷)
Theorem	rspc2 2875*	2-variable restricted specialization, using implicit substitution. (Contributed by NM, 9-Nov-2012.)
⊢ Ⅎ𝑥𝜒    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))
Theorem	rspc2gv 2876*	Restricted specialization with two quantifiers, using implicit substitution. (Contributed by BJ, 2-Dec-2021.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑊 𝜑 → 𝜓))
Theorem	rspc2v 2877*	2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))
Theorem	rspc2va 2878*	2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))    ⇒   ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓)
Theorem	rspc2ev 2879*	2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)
Theorem	rspc3v 2880*	3-variable restricted specialization, using implicit substitution. (Contributed by NM, 10-May-2005.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓))
Theorem	rspc3ev 2881*	3-variable restricted existentional specialization, using implicit substitution. (Contributed by NM, 25-Jul-2012.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓))    ⇒   ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑇 𝜑)
Theorem	rspceeqv 2882*	Restricted existential specialization in an equality, using implicit substitution. (Contributed by BJ, 2-Sep-2022.)
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐸 = 𝐷) → ∃𝑥 ∈ 𝐵 𝐸 = 𝐶)
Theorem	eqvinc 2883*	A variable introduction law for class equality. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵))
Theorem	eqvincg 2884*	A variable introduction law for class equality, deduction version. (Contributed by Thierry Arnoux, 2-Mar-2017.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵)))
Theorem	eqvincf 2885	A variable introduction law for class equality, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 14-Sep-2003.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵))
Theorem	alexeq 2886*	Two ways to express substitution of 𝐴 for 𝑥 in 𝜑. (Contributed by NM, 2-Mar-1995.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
Theorem	ceqex 2887*	Equality implies equivalence with substitution. (Contributed by NM, 2-Mar-1995.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)))
Theorem	ceqsexg 2888*	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 2889*	Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 29-Dec-1996.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓))
Theorem	ceqsrexv 2890*	Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 30-Apr-2004.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓))
Theorem	ceqsrexbv 2891*	Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by Mario Carneiro, 14-Mar-2014.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥 ∈ 𝐵 (𝑥 = 𝐴 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
Theorem	ceqsrex2v 2892*	Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 29-Oct-2005.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝜑) ↔ 𝜒))
Theorem	clel2 2893*	An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
Theorem	clel3g 2894*	An alternate definition of class membership when the class is a set. (Contributed by NM, 13-Aug-2005.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥)))
Theorem	clel3 2895*	An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴 ∈ 𝑥))
Theorem	clel4 2896*	An alternate definition of class membership when the class is a set. (Contributed by NM, 18-Aug-1993.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐵 → 𝐴 ∈ 𝑥))
Theorem	clel5 2897*	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.) (Revised by Steven Nguyen, 19-May-2023.)
⊢ (𝑋 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑋 = 𝑥)
Theorem	pm13.183 2898*	Compare theorem *13.183 in [WhiteheadRussell] p. 178. Only 𝐴 is required to be a set. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 ↔ ∀𝑧(𝑧 = 𝐴 ↔ 𝑧 = 𝐵)))
Theorem	rr19.3v 2899*	Restricted quantifier version of Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 25-Oct-2012.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑)
Theorem	rr19.28v 2900*	Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 29-Oct-2012.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 𝜓))