# 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 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
vtoclgf.2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
vtoclgf.3 ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
vtoclgf.4 ${⊢}{\phi }$
Assertion vtoclgf ${⊢}{A}\in {V}\to {\psi }$

### Proof

Step Hyp Ref Expression
1 vtoclgf.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 vtoclgf.2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
3 vtoclgf.3 ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
4 vtoclgf.4 ${⊢}{\phi }$
5 elex ${⊢}{A}\in {V}\to {A}\in \mathrm{V}$
6 1 issetf ${⊢}{A}\in \mathrm{V}↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}$
7 4 3 mpbii ${⊢}{x}={A}\to {\psi }$
8 2 7 exlimi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\to {\psi }$
9 6 8 sylbi ${⊢}{A}\in \mathrm{V}\to {\psi }$
10 5 9 syl ${⊢}{A}\in {V}\to {\psi }$