# Metamath Proof Explorer

## Theorem vtoclgft

Description: Closed theorem form of vtoclgf . (Contributed by NM, 17-Feb-2013) (Revised by Mario Carneiro, 12-Oct-2016) (Proof shortened by JJ, 11-Aug-2021) Avoid ax-13 . (Revised by Gino Giotto, 6-Oct-2023)

Ref Expression
Assertion vtoclgft ${⊢}\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 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
3 nfnfc1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
4 nfcvd ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{z}$
5 id ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
6 4 5 nfeqd ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}={A}$
7 6 nfnd ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬{z}={A}$
8 nfvd ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to Ⅎ{z}\phantom{\rule{.4em}{0ex}}¬{x}={A}$
9 eqeq1 ${⊢}{z}={x}\to \left({z}={A}↔{x}={A}\right)$
10 9 a1i ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left({z}={x}\to \left({z}={A}↔{x}={A}\right)\right)$
11 notbi ${⊢}\left({z}={A}↔{x}={A}\right)↔\left(¬{z}={A}↔¬{x}={A}\right)$
12 10 11 syl6ib ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left({z}={x}\to \left(¬{z}={A}↔¬{x}={A}\right)\right)$
13 biimp ${⊢}\left(¬{z}={A}↔¬{x}={A}\right)\to \left(¬{z}={A}\to ¬{x}={A}\right)$
14 12 13 syl6 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left({z}={x}\to \left(¬{z}={A}\to ¬{x}={A}\right)\right)$
15 2 3 7 8 14 cbv1v ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}¬{z}={A}\to \forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={A}\right)$
16 equcomi ${⊢}{x}={z}\to {z}={x}$
17 biimpr ${⊢}\left(¬{z}={A}↔¬{x}={A}\right)\to \left(¬{x}={A}\to ¬{z}={A}\right)$
18 16 12 17 syl56 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left({x}={z}\to \left(¬{x}={A}\to ¬{z}={A}\right)\right)$
19 3 2 8 7 18 cbv1v ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={A}\to \forall {z}\phantom{\rule{.4em}{0ex}}¬{z}={A}\right)$
20 15 19 impbid ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}¬{z}={A}↔\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={A}\right)$
21 alnex ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}¬{z}={A}↔¬\exists {z}\phantom{\rule{.4em}{0ex}}{z}={A}$
22 alnex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={A}↔¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}$
23 20 21 22 3bitr3g ${⊢}\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)$
24 23 con4bid ${⊢}\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)$
25 1 24 syl5ib ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left({A}\in {V}\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\right)$
26 25 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)$
27 26 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}$
28 biimp ${⊢}\left({\phi }↔{\psi }\right)\to \left({\phi }\to {\psi }\right)$
29 28 imim2i ${⊢}\left({x}={A}\to \left({\phi }↔{\psi }\right)\right)\to \left({x}={A}\to \left({\phi }\to {\psi }\right)\right)$
30 29 com23 ${⊢}\left({x}={A}\to \left({\phi }↔{\psi }\right)\right)\to \left({\phi }\to \left({x}={A}\to {\psi }\right)\right)$
31 30 imp ${⊢}\left(\left({x}={A}\to \left({\phi }↔{\psi }\right)\right)\wedge {\phi }\right)\to \left({x}={A}\to {\psi }\right)$
32 31 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)$
33 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)$
34 33 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)$
35 32 34 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)$
36 35 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)$
37 36 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)$
38 27 37 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 }$