P. 28 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2701-2800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elexi 2701	If a class is a member of another class, it is a set. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ 𝐵    ⇒   ⊢ 𝐴 ∈ V
Theorem	elexd 2702	If a class is a member of another class, it is a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐴 ∈ V)
Theorem	elisset 2703*	An element of a class exists. (Contributed by NM, 1-May-1995.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
Theorem	elex22 2704*	If two classes each contain another class, then both contain some set. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
Theorem	elex2 2705*	If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.)
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)
Theorem	ralv 2706	A universal quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.)
⊢ (∀𝑥 ∈ V 𝜑 ↔ ∀𝑥𝜑)
Theorem	rexv 2707	An existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004.)
⊢ (∃𝑥 ∈ V 𝜑 ↔ ∃𝑥𝜑)
Theorem	reuv 2708	A unique existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 1-Nov-2010.)
⊢ (∃!𝑥 ∈ V 𝜑 ↔ ∃!𝑥𝜑)
Theorem	rmov 2709	An at-most-one quantifier restricted to the universe is unrestricted. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
⊢ (∃*𝑥 ∈ V 𝜑 ↔ ∃*𝑥𝜑)
Theorem	rabab 2710	A class abstraction restricted to the universe is unrestricted. (Contributed by NM, 27-Dec-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ {𝑥 ∈ V ∣ 𝜑} = {𝑥 ∣ 𝜑}
Theorem	ralcom4 2711*	Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑)
Theorem	rexcom4 2712*	Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
Theorem	rexcom4a 2713*	Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.)
⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ ∃𝑥𝜓))
Theorem	rexcom4b 2714*	Specialized existential commutation lemma. (Contributed by Jeff Madsen, 1-Jun-2011.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 𝜑)
Theorem	ceqsalt 2715*	Closed theorem version of ceqsalg 2717. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝑉) → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	ceqsralt 2716*	Restricted quantifier version of ceqsalt 2715. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝐴 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	ceqsalg 2717*	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 29-Oct-2003.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	ceqsal 2718*	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	ceqsalv 2719*	A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)
Theorem	ceqsralv 2720*	Restricted quantifier version of ceqsalv 2719. (Contributed by NM, 21-Jun-2013.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝑥 = 𝐴 → 𝜑) ↔ 𝜓))
Theorem	gencl 2721*	Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.)
⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝐵))    &   ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))    &   ⊢ (𝜒 → 𝜑)    ⇒   ⊢ (𝜃 → 𝜓)
Theorem	2gencl 2722*	Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.)
⊢ (𝐶 ∈ 𝑆 ↔ ∃𝑥 ∈ 𝑅 𝐴 = 𝐶)    &   ⊢ (𝐷 ∈ 𝑆 ↔ ∃𝑦 ∈ 𝑅 𝐵 = 𝐷)    &   ⊢ (𝐴 = 𝐶 → (𝜑 ↔ 𝜓))    &   ⊢ (𝐵 = 𝐷 → (𝜓 ↔ 𝜒))    &   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → 𝜑)    ⇒   ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆) → 𝜒)
Theorem	3gencl 2723*	Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996.)
⊢ (𝐷 ∈ 𝑆 ↔ ∃𝑥 ∈ 𝑅 𝐴 = 𝐷)    &   ⊢ (𝐹 ∈ 𝑆 ↔ ∃𝑦 ∈ 𝑅 𝐵 = 𝐹)    &   ⊢ (𝐺 ∈ 𝑆 ↔ ∃𝑧 ∈ 𝑅 𝐶 = 𝐺)    &   ⊢ (𝐴 = 𝐷 → (𝜑 ↔ 𝜓))    &   ⊢ (𝐵 = 𝐹 → (𝜓 ↔ 𝜒))    &   ⊢ (𝐶 = 𝐺 → (𝜒 ↔ 𝜃))    &   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑅) → 𝜑)    ⇒   ⊢ ((𝐷 ∈ 𝑆 ∧ 𝐹 ∈ 𝑆 ∧ 𝐺 ∈ 𝑆) → 𝜃)
Theorem	cgsexg 2724*	Implicit substitution inference for general classes. (Contributed by NM, 26-Aug-2007.)
⊢ (𝑥 = 𝐴 → 𝜒)    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∃𝑥(𝜒 ∧ 𝜑) ↔ 𝜓))
Theorem	cgsex2g 2725*	Implicit substitution inference for general classes. (Contributed by NM, 26-Jul-1995.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 𝜒)    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥∃𝑦(𝜒 ∧ 𝜑) ↔ 𝜓))
Theorem	cgsex4g 2726*	An implicit substitution inference for 4 general classes. (Contributed by NM, 5-Aug-1995.)
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → 𝜒)    &   ⊢ (𝜒 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑) ↔ 𝜓))
Theorem	ceqsex 2727*	Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)
Theorem	ceqsexv 2728*	Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓)
Theorem	ceqsex2 2729*	Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑) ↔ 𝜒)
Theorem	ceqsex2v 2730*	Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝜑) ↔ 𝜒)
Theorem	ceqsex3v 2731*	Elimination of three existential quantifiers, using implicit substitution. (Contributed by NM, 16-Aug-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝜑) ↔ 𝜃)
Theorem	ceqsex4v 2732*	Elimination of four existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷) ∧ 𝜑) ↔ 𝜏)
Theorem	ceqsex6v 2733*	Elimination of six existential quantifiers, using implicit substitution. (Contributed by NM, 21-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐸 ∈ V    &   ⊢ 𝐹 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑣 = 𝐸 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑢 = 𝐹 → (𝜂 ↔ 𝜁))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ (𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ 𝜑) ↔ 𝜁)
Theorem	ceqsex8v 2734*	Elimination of eight existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝐸 ∈ V    &   ⊢ 𝐹 ∈ V    &   ⊢ 𝐺 ∈ V    &   ⊢ 𝐻 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (𝑤 = 𝐷 → (𝜃 ↔ 𝜏))    &   ⊢ (𝑣 = 𝐸 → (𝜏 ↔ 𝜂))    &   ⊢ (𝑢 = 𝐹 → (𝜂 ↔ 𝜁))    &   ⊢ (𝑡 = 𝐺 → (𝜁 ↔ 𝜎))    &   ⊢ (𝑠 = 𝐻 → (𝜎 ↔ 𝜌))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤∃𝑣∃𝑢∃𝑡∃𝑠(((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ∧ ((𝑣 = 𝐸 ∧ 𝑢 = 𝐹) ∧ (𝑡 = 𝐺 ∧ 𝑠 = 𝐻)) ∧ 𝜑) ↔ 𝜌)
Theorem	gencbvex 2735*	Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ 𝐴 ∈ V    &   ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝑦))    ⇒   ⊢ (∃𝑥(𝜒 ∧ 𝜑) ↔ ∃𝑦(𝜃 ∧ 𝜓))
Theorem	gencbvex2 2736*	Restatement of gencbvex 2735 with weaker hypotheses. (Contributed by Jeff Hankins, 6-Dec-2006.)
⊢ 𝐴 ∈ V    &   ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜃 → ∃𝑥(𝜒 ∧ 𝐴 = 𝑦))    ⇒   ⊢ (∃𝑥(𝜒 ∧ 𝜑) ↔ ∃𝑦(𝜃 ∧ 𝜓))
Theorem	gencbval 2737*	Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996.) (Proof rewritten by Jim Kingdon, 20-Jun-2018.)
⊢ 𝐴 ∈ V    &   ⊢ (𝐴 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (𝐴 = 𝑦 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜃 ↔ ∃𝑥(𝜒 ∧ 𝐴 = 𝑦))    ⇒   ⊢ (∀𝑥(𝜒 → 𝜑) ↔ ∀𝑦(𝜃 → 𝜓))
Theorem	sbhypf 2738*	Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf . (Contributed by Raph Levien, 10-Apr-2004.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ 𝜓))
Theorem	vtoclgft 2739	Closed theorem form of vtoclgf 2747. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 12-Oct-2016.)
⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → 𝜓)
Theorem	vtocldf 2740	Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝜓)    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝐴)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	vtocld 2741*	Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	vtoclf 2742*	Implicit substitution of a class for a setvar variable. This is a generalization of chvar 1731. (Contributed by NM, 30-Aug-1993.)
⊢ Ⅎ𝑥𝜓    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	vtocl 2743*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	vtocl2 2744*	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 2745*	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 2746*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 23-Dec-1993.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜒 ↔ 𝜃)
Theorem	vtoclgf 2747	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 2748*	Version of vtoclgf 2747 with one non-freeness hypothesis replaced with a disjoint variable condition, thus avoiding dependency on ax-11 1485 and ax-13 1492. (Contributed by BJ, 1-May-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	vtoclg 2749*	Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜓)
Theorem	vtoclbg 2750*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))
Theorem	vtocl2gf 2751	Implicit substitution of a class for a setvar variable. (Contributed by NM, 25-Apr-1995.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ 𝜑    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒)
Theorem	vtocl3gf 2752	Implicit substitution of a class for a setvar variable. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑧𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ Ⅎ𝑧𝜃    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ 𝜑    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 𝜃)
Theorem	vtocl2g 2753*	Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ 𝜑    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒)
Theorem	vtoclgaf 2754*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 17-Feb-2006.) (Revised by Mario Carneiro, 10-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ 𝐵 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝐵 → 𝜓)
Theorem	vtoclga 2755*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ 𝐵 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝐵 → 𝜓)
Theorem	vtocl2gaf 2756*	Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 10-Aug-2013.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒)
Theorem	vtocl2ga 2757*	Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒)
Theorem	vtocl3gaf 2758*	Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 10-Aug-2013.) (Revised by Mario Carneiro, 11-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑧𝐴    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑧𝐵    &   ⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜒    &   ⊢ Ⅎ𝑧𝜃    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑇) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → 𝜃)
Theorem	vtocl3ga 2759*	Implicit substitution of 3 classes for 3 setvar variables. (Contributed by NM, 20-Aug-1995.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝑅 ∧ 𝑧 ∈ 𝑆) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑆) → 𝜃)
Theorem	vtocleg 2760*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 10-Jan-2004.)
⊢ (𝑥 = 𝐴 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝜑)
Theorem	vtoclegft 2761*	Implicit substitution of a class for a setvar variable. (Closed theorem version of vtoclef 2762.) (Contributed by NM, 7-Nov-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
⊢ ((𝐴 ∈ 𝐵 ∧ Ⅎ𝑥𝜑 ∧ ∀𝑥(𝑥 = 𝐴 → 𝜑)) → 𝜑)
Theorem	vtoclef 2762*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 18-Aug-1993.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	vtocle 2763*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 9-Sep-1993.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	vtoclri 2764*	Implicit substitution of a class for a setvar variable. (Contributed by NM, 21-Nov-1994.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ∀𝑥 ∈ 𝐵 𝜑    ⇒   ⊢ (𝐴 ∈ 𝐵 → 𝜓)
Theorem	spcimgft 2765	A closed version of spcimgf 2769. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 → 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥𝜑 → 𝜓)))
Theorem	spcgft 2766	A closed version of spcgf 2771. (Contributed by Andrew Salmon, 6-Jun-2011.) (Revised by Mario Carneiro, 4-Jan-2017.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥𝜑 → 𝜓)))
Theorem	spcimegft 2767	A closed version of spcimegf 2770. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜓 → 𝜑)) → (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥𝜑)))
Theorem	spcegft 2768	A closed version of spcegf 2772. (Contributed by Jim Kingdon, 22-Jun-2018.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (𝜓 → ∃𝑥𝜑)))
Theorem	spcimgf 2769	Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 → 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓))
Theorem	spcimegf 2770	Existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜓 → 𝜑))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))
Theorem	spcgf 2771	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 2772	Existential specialization, using implicit substitution. (Contributed by NM, 2-Feb-1997.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))
Theorem	spcimdv 2773*	Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	spcdv 2774*	Rule of specialization, using implicit substitution. Analogous to rspcdv 2796. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒))
Theorem	spcimedv 2775*	Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → (𝜒 → ∃𝑥𝜓))
Theorem	spcgv 2776*	Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → 𝜓))
Theorem	spcegv 2777*	Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))
Theorem	spcedv 2778*	Existential specialization, using implicit substitution, deduction version. (Contributed by RP, 12-Aug-2020.)
⊢ (𝜑 → 𝑋 ∈ V)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	spc2egv 2779*	Existential specialization with 2 quantifiers, using implicit substitution. (Contributed by NM, 3-Aug-1995.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝜓 → ∃𝑥∃𝑦𝜑))
Theorem	spc2gv 2780*	Specialization with 2 quantifiers, using implicit substitution. (Contributed by NM, 27-Apr-2004.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑥∀𝑦𝜑 → 𝜓))
Theorem	spc3egv 2781*	Existential specialization with 3 quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝜓 → ∃𝑥∃𝑦∃𝑧𝜑))
Theorem	spc3gv 2782*	Specialization with 3 quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008.)
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀𝑥∀𝑦∀𝑧𝜑 → 𝜓))
Theorem	spcv 2783*	Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spcev 2784*	Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜓 → ∃𝑥𝜑)
Theorem	spc2ev 2785*	Existential specialization, using implicit substitution. (Contributed by NM, 3-Aug-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜓 → ∃𝑥∃𝑦𝜑)
Theorem	rspct 2786*	A closed version of rspc 2787. (Contributed by Andrew Salmon, 6-Jun-2011.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)))
Theorem	rspc 2787*	Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
Theorem	rspce 2788*	Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) (Revised by Mario Carneiro, 11-Oct-2016.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)
Theorem	rspcv 2789*	Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
Theorem	rspccv 2790*	Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓))
Theorem	rspcva 2791*	Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 𝜑) → 𝜓)
Theorem	rspccva 2792*	Restricted specialization, using implicit substitution. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((∀𝑥 ∈ 𝐵 𝜑 ∧ 𝐴 ∈ 𝐵) → 𝜓)
Theorem	rspcev 2793*	Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)
Theorem	rspcimdv 2794*	Restricted specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))
Theorem	rspcimedv 2795*	Restricted existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓))
Theorem	rspcdv 2796*	Restricted specialization, using implicit substitution. (Contributed by NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 → 𝜒))
Theorem	rspcedv 2797*	Restricted existential specialization, using implicit substitution. (Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓))
Theorem	rspcdva 2798*	Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.)
⊢ (𝑥 = 𝐶 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	rspcedvd 2799*	Restricted existential specialization, using implicit substitution. Variant of rspcedv 2797. (Contributed by AV, 27-Nov-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
Theorem	rspcime 2800*	Prove a restricted existential. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝜓)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)