This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ 𝐵 → 𝜓 )