Metamath Proof Explorer


Theorem vtoclgft

Description: Closed theorem form of vtoclgf . The reverse implication is proven in ceqsal1t . See ceqsalt for a version with x and A disjoint. (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 elissetv
 |-  ( 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 notbid
 |-  ( z = x -> ( -. z = A <-> -. x = A ) )
11 10 a1i
 |-  ( F/_ x A -> ( z = x -> ( -. z = A <-> -. x = A ) ) )
12 2 3 7 8 11 cbv2w
 |-  ( F/_ x A -> ( A. z -. z = A <-> A. x -. x = A ) )
13 alnex
 |-  ( A. z -. z = A <-> -. E. z z = A )
14 alnex
 |-  ( A. x -. x = A <-> -. E. x x = A )
15 12 13 14 3bitr3g
 |-  ( F/_ x A -> ( -. E. z z = A <-> -. E. x x = A ) )
16 15 con4bid
 |-  ( F/_ x A -> ( E. z z = A <-> E. x x = A ) )
17 1 16 imbitrid
 |-  ( F/_ x A -> ( A e. V -> E. x x = A ) )
18 17 ad2antrr
 |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) ) -> ( A e. V -> E. x x = A ) )
19 18 3impia
 |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) /\ A e. V ) -> E. x x = A )
20 biimp
 |-  ( ( ph <-> ps ) -> ( ph -> ps ) )
21 20 imim2i
 |-  ( ( x = A -> ( ph <-> ps ) ) -> ( x = A -> ( ph -> ps ) ) )
22 21 com23
 |-  ( ( x = A -> ( ph <-> ps ) ) -> ( ph -> ( x = A -> ps ) ) )
23 22 imp
 |-  ( ( ( x = A -> ( ph <-> ps ) ) /\ ph ) -> ( x = A -> ps ) )
24 23 alanimi
 |-  ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) -> A. x ( x = A -> ps ) )
25 19.23t
 |-  ( F/ x ps -> ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) ) )
26 25 adantl
 |-  ( ( F/_ x A /\ F/ x ps ) -> ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) ) )
27 24 26 imbitrid
 |-  ( ( F/_ x A /\ F/ x ps ) -> ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) -> ( E. x x = A -> ps ) ) )
28 27 imp
 |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) ) -> ( E. x x = A -> ps ) )
29 28 3adant3
 |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) /\ A e. V ) -> ( E. x x = A -> ps ) )
30 19 29 mpd
 |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) /\ A e. V ) -> ps )