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

### Proof

Step Hyp Ref Expression
1 vtoclgaf.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 vtoclgaf.2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
3 vtoclgaf.3 ${⊢}{x}={A}\to \left({\phi }↔{\psi }\right)$
4 vtoclgaf.4 ${⊢}{x}\in {B}\to {\phi }$
5 1 nfel1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}\in {B}$
6 5 2 nfim ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({A}\in {B}\to {\psi }\right)$
7 eleq1 ${⊢}{x}={A}\to \left({x}\in {B}↔{A}\in {B}\right)$
8 7 3 imbi12d ${⊢}{x}={A}\to \left(\left({x}\in {B}\to {\phi }\right)↔\left({A}\in {B}\to {\psi }\right)\right)$
9 1 6 8 4 vtoclgf ${⊢}{A}\in {B}\to \left({A}\in {B}\to {\psi }\right)$
10 9 pm2.43i ${⊢}{A}\in {B}\to {\psi }$