# Metamath Proof Explorer

## Theorem vtoclgftOLD

Description: Obsolete version of vtoclgft . (Contributed by NM, 17-Feb-2013) (Revised by Mario Carneiro, 12-Oct-2016) (Proof shortened by JJ, 11-Aug-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion vtoclgftOLD ${⊢}\left(\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\wedge Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\wedge \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to \left({\phi }↔{\psi }\right)\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\wedge {A}\in {V}\right)\to {\psi }$

### Proof

Step Hyp Ref Expression
1 elisset ${⊢}{A}\in {V}\to \exists {z}\phantom{\rule{.4em}{0ex}}{z}={A}$
2 nfnfc1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
3 nfcvd ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{z}$
4 id ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
5 3 4 nfeqd ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}={A}$
6 eqeq1 ${⊢}{z}={x}\to \left({z}={A}↔{x}={A}\right)$
7 6 a1i ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left({z}={x}\to \left({z}={A}↔{x}={A}\right)\right)$
8 2 5 7 cbvexd ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}{z}={A}↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\right)$
9 1 8 syl5ib ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left({A}\in {V}\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\right)$
10 9 ad2antrr ${⊢}\left(\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\wedge Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\wedge \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to \left({\phi }↔{\psi }\right)\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\to \left({A}\in {V}\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\right)$
11 10 3impia ${⊢}\left(\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\wedge Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\wedge \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to \left({\phi }↔{\psi }\right)\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\wedge {A}\in {V}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}$
12 biimp ${⊢}\left({\phi }↔{\psi }\right)\to \left({\phi }\to {\psi }\right)$
13 12 imim2i ${⊢}\left({x}={A}\to \left({\phi }↔{\psi }\right)\right)\to \left({x}={A}\to \left({\phi }\to {\psi }\right)\right)$
14 13 com23 ${⊢}\left({x}={A}\to \left({\phi }↔{\psi }\right)\right)\to \left({\phi }\to \left({x}={A}\to {\psi }\right)\right)$
15 14 imp ${⊢}\left(\left({x}={A}\to \left({\phi }↔{\psi }\right)\right)\wedge {\phi }\right)\to \left({x}={A}\to {\psi }\right)$
16 15 alanimi ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to \left({\phi }↔{\psi }\right)\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to {\psi }\right)$
17 19.23t ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to {\psi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\to {\psi }\right)\right)$
18 17 adantl ${⊢}\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\wedge Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to {\psi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\to {\psi }\right)\right)$
19 16 18 syl5ib ${⊢}\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\wedge Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \left(\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to \left({\phi }↔{\psi }\right)\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\to {\psi }\right)\right)$
20 19 imp ${⊢}\left(\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\wedge Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\wedge \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to \left({\phi }↔{\psi }\right)\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\to {\psi }\right)$
21 20 3adant3 ${⊢}\left(\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\wedge Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\wedge \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to \left({\phi }↔{\psi }\right)\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\wedge {A}\in {V}\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\to {\psi }\right)$
22 11 21 mpd ${⊢}\left(\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\wedge Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\wedge \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to \left({\phi }↔{\psi }\right)\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\wedge {A}\in {V}\right)\to {\psi }$