Theorem vtocleg

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Hypothesis	vtocleg.1	⊢ ( 𝑥 = 𝐴 → 𝜑 )
Assertion	vtocleg	⊢ ( 𝐴 ∈ 𝑉 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		vtocleg.1	⊢ ( 𝑥 = 𝐴 → 𝜑 )
2		elisset	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 )
3	1	exlimiv	⊢ ( ∃ 𝑥 𝑥 = 𝐴 → 𝜑 )
4	2 3	syl	⊢ ( 𝐴 ∈ 𝑉 → 𝜑 )