# 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
`|- ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) /\ A e. V ) -> ps )`

### Proof

Step Hyp Ref Expression
1 elisset
` |-  ( A e. V -> E. z z = A )`
2 nfv
` |-  F/ z F/_ x A`
3 nfnfc1
` |-  F/ x F/_ x A`
4 nfcvd
` |-  ( F/_ x A -> F/_ x z )`
5 id
` |-  ( F/_ x A -> F/_ x A )`
6 4 5 nfeqd
` |-  ( F/_ x A -> F/ x z = A )`
7 6 nfnd
` |-  ( F/_ x A -> F/ x -. z = A )`
8 nfvd
` |-  ( F/_ x A -> F/ z -. x = A )`
9 eqeq1
` |-  ( z = x -> ( z = A <-> x = A ) )`
10 9 a1i
` |-  ( F/_ x A -> ( z = x -> ( z = A <-> x = A ) ) )`
11 notbi
` |-  ( ( z = A <-> x = A ) <-> ( -. z = A <-> -. x = A ) )`
12 10 11 syl6ib
` |-  ( F/_ x A -> ( z = x -> ( -. z = A <-> -. x = A ) ) )`
13 biimp
` |-  ( ( -. z = A <-> -. x = A ) -> ( -. z = A -> -. x = A ) )`
14 12 13 syl6
` |-  ( F/_ x A -> ( z = x -> ( -. z = A -> -. x = A ) ) )`
15 2 3 7 8 14 cbv1v
` |-  ( F/_ x A -> ( A. z -. z = A -> A. x -. x = A ) )`
16 equcomi
` |-  ( x = z -> z = x )`
17 biimpr
` |-  ( ( -. z = A <-> -. x = A ) -> ( -. x = A -> -. z = A ) )`
18 16 12 17 syl56
` |-  ( F/_ x A -> ( x = z -> ( -. x = A -> -. z = A ) ) )`
19 3 2 8 7 18 cbv1v
` |-  ( F/_ x A -> ( A. x -. x = A -> A. z -. z = A ) )`
20 15 19 impbid
` |-  ( F/_ x A -> ( A. z -. z = A <-> A. x -. x = A ) )`
21 alnex
` |-  ( A. z -. z = A <-> -. E. z z = A )`
22 alnex
` |-  ( A. x -. x = A <-> -. E. x x = A )`
23 20 21 22 3bitr3g
` |-  ( F/_ x A -> ( -. E. z z = A <-> -. E. x x = A ) )`
24 23 con4bid
` |-  ( F/_ x A -> ( E. z z = A <-> E. x x = A ) )`
25 1 24 syl5ib
` |-  ( F/_ x A -> ( A e. V -> E. x x = A ) )`
` |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) ) -> ( A e. V -> E. x x = A ) )`
27 26 3impia
` |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) /\ A e. V ) -> E. x x = A )`
28 biimp
` |-  ( ( ph <-> ps ) -> ( ph -> ps ) )`
29 28 imim2i
` |-  ( ( x = A -> ( ph <-> ps ) ) -> ( x = A -> ( ph -> ps ) ) )`
30 29 com23
` |-  ( ( x = A -> ( ph <-> ps ) ) -> ( ph -> ( x = A -> ps ) ) )`
31 30 imp
` |-  ( ( ( x = A -> ( ph <-> ps ) ) /\ ph ) -> ( x = A -> ps ) )`
32 31 alanimi
` |-  ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) -> A. x ( x = A -> ps ) )`
33 19.23t
` |-  ( F/ x ps -> ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) ) )`
` |-  ( ( F/_ x A /\ F/ x ps ) -> ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) ) )`
` |-  ( ( F/_ x A /\ F/ x ps ) -> ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) -> ( E. x x = A -> ps ) ) )`
` |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) ) -> ( E. x x = A -> ps ) )`
` |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) /\ A e. V ) -> ( E. x x = A -> ps ) )`
` |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) /\ A e. V ) -> ps )`