Theorem vtoclef

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

	Ref	Expression
Hypotheses	vtoclef.1	⊢ Ⅎ 𝑥 𝜑
	vtoclef.2	⊢ 𝐴 ∈ V
	vtoclef.3	⊢ ( 𝑥 = 𝐴 → 𝜑 )
Assertion	vtoclef	⊢ 𝜑

Proof

Step	Hyp	Ref	Expression
1		vtoclef.1	⊢ Ⅎ 𝑥 𝜑
2		vtoclef.2	⊢ 𝐴 ∈ V
3		vtoclef.3	⊢ ( 𝑥 = 𝐴 → 𝜑 )
4	2	isseti	⊢ ∃ 𝑥 𝑥 = 𝐴
5	1 3	exlimi	⊢ ( ∃ 𝑥 𝑥 = 𝐴 → 𝜑 )
6	4 5	ax-mp	⊢ 𝜑