Metamath Proof Explorer


Theorem vtoclgf

Description: Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of disjoint variable restrictions. (Contributed by NM, 21-Sep-2003) (Proof shortened by Mario Carneiro, 10-Oct-2016)

Ref Expression
Hypotheses vtoclgf.1 𝑥 𝐴
vtoclgf.2 𝑥 𝜓
vtoclgf.3 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
vtoclgf.4 𝜑
Assertion vtoclgf ( 𝐴𝑉𝜓 )

Proof

Step Hyp Ref Expression
1 vtoclgf.1 𝑥 𝐴
2 vtoclgf.2 𝑥 𝜓
3 vtoclgf.3 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
4 vtoclgf.4 𝜑
5 elex ( 𝐴𝑉𝐴 ∈ V )
6 1 issetf ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )
7 4 3 mpbii ( 𝑥 = 𝐴𝜓 )
8 2 7 exlimi ( ∃ 𝑥 𝑥 = 𝐴𝜓 )
9 6 8 sylbi ( 𝐴 ∈ V → 𝜓 )
10 5 9 syl ( 𝐴𝑉𝜓 )