Theorem vtoclgaf

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 17-Feb-2006) (Revised by Mario Carneiro, 10-Oct-2016)

	Ref	Expression
Hypotheses	vtoclgaf.1	⊢ Ⅎ 𝑥 𝐴
	vtoclgaf.2	⊢ Ⅎ 𝑥 𝜓
	vtoclgaf.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	vtoclgaf.4	⊢ ( 𝑥 ∈ 𝐵 → 𝜑 )
Assertion	vtoclgaf	⊢ ( 𝐴 ∈ 𝐵 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		vtoclgaf.1	⊢ Ⅎ 𝑥 𝐴
2		vtoclgaf.2	⊢ Ⅎ 𝑥 𝜓
3		vtoclgaf.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4		vtoclgaf.4	⊢ ( 𝑥 ∈ 𝐵 → 𝜑 )
5	1	nfel1	⊢ Ⅎ 𝑥 𝐴 ∈ 𝐵
6	5 2	nfim	⊢ Ⅎ 𝑥 ( 𝐴 ∈ 𝐵 → 𝜓 )
7		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
8	7 3	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 → 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 → 𝜓 ) ) )
9	1 6 8 4	vtoclgf	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ 𝐵 → 𝜓 ) )
10	9	pm2.43i	⊢ ( 𝐴 ∈ 𝐵 → 𝜓 )