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 elex 
 |-  ( A e. V -> A e. _V )
2 issetft 
 |-  ( F/_ x A -> ( A e. _V <-> E. x x = A ) )
3 1 2 imbitrid 
 |-  ( F/_ x A -> ( A e. V -> E. x x = A ) )
4 3 ad2antrr 
 |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) ) -> ( A e. V -> E. x x = A ) )
5 4 3impia 
 |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) /\ A e. V ) -> E. x x = A )
6 biimp 
 |-  ( ( ph <-> ps ) -> ( ph -> ps ) )
7 6 imim2i 
 |-  ( ( x = A -> ( ph <-> ps ) ) -> ( x = A -> ( ph -> ps ) ) )
8 7 com23 
 |-  ( ( x = A -> ( ph <-> ps ) ) -> ( ph -> ( x = A -> ps ) ) )
9 8 imp 
 |-  ( ( ( x = A -> ( ph <-> ps ) ) /\ ph ) -> ( x = A -> ps ) )
10 9 alanimi 
 |-  ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) -> A. x ( x = A -> ps ) )
11 19.23t 
 |-  ( F/ x ps -> ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) ) )
12 11 adantl 
 |-  ( ( F/_ x A /\ F/ x ps ) -> ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) ) )
13 10 12 imbitrid 
 |-  ( ( F/_ x A /\ F/ x ps ) -> ( ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) -> ( E. x x = A -> ps ) ) )
14 13 imp 
 |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) ) -> ( E. x x = A -> ps ) )
15 14 3adant3 
 |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) /\ A e. V ) -> ( E. x x = A -> ps ) )
16 5 15 mpd 
 |-  ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A -> ( ph <-> ps ) ) /\ A. x ph ) /\ A e. V ) -> ps )