# Metamath Proof Explorer

## Theorem vtocldf

Description: Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses vtocld.1 ${⊢}{\phi }\to {A}\in {V}$
vtocld.2 ${⊢}\left({\phi }\wedge {x}={A}\right)\to \left({\psi }↔{\chi }\right)$
vtocld.3 ${⊢}{\phi }\to {\psi }$
vtocldf.4 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
vtocldf.5 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
vtocldf.6 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
Assertion vtocldf ${⊢}{\phi }\to {\chi }$

### Proof

Step Hyp Ref Expression
1 vtocld.1 ${⊢}{\phi }\to {A}\in {V}$
2 vtocld.2 ${⊢}\left({\phi }\wedge {x}={A}\right)\to \left({\psi }↔{\chi }\right)$
3 vtocld.3 ${⊢}{\phi }\to {\psi }$
4 vtocldf.4 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
5 vtocldf.5 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
6 vtocldf.6 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
7 2 ex ${⊢}{\phi }\to \left({x}={A}\to \left({\psi }↔{\chi }\right)\right)$
8 4 7 alrimi ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to \left({\psi }↔{\chi }\right)\right)$
9 4 3 alrimi ${⊢}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }$
10 vtoclgft ${⊢}\left(\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\wedge Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }\right)\wedge \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to \left({\psi }↔{\chi }\right)\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\wedge {A}\in {V}\right)\to {\chi }$
11 5 6 8 9 1 10 syl221anc ${⊢}{\phi }\to {\chi }$