Metamath Proof Explorer

Theorem ceqsalt

Description: Closed theorem version of ceqsalg . (Contributed by NM, 28-Feb-2013) (Revised by Mario Carneiro, 10-Oct-2016)

Ref Expression
Assertion ceqsalt 
|- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) <-> ps ) )

Proof

Step Hyp Ref Expression
1 elisset 
 |-  ( A e. V -> E. x x = A )
2 1 3ad2ant3 
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> E. x x = A )
3 biimp 
 |-  ( ( ph <-> ps ) -> ( ph -> ps ) )
4 3 imim3i 
 |-  ( ( x = A -> ( ph <-> ps ) ) -> ( ( x = A -> ph ) -> ( x = A -> ps ) ) )
5 4 al2imi 
 |-  ( A. x ( x = A -> ( ph <-> ps ) ) -> ( A. x ( x = A -> ph ) -> A. x ( x = A -> ps ) ) )
6 5 3ad2ant2 
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) -> A. x ( x = A -> ps ) ) )
7 19.23t 
 |-  ( F/ x ps -> ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) ) )
8 7 3ad2ant1 
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) ) )
9 6 8 sylibd 
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) -> ( E. x x = A -> ps ) ) )
10 2 9 mpid 
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) -> ps ) )
11 biimpr 
 |-  ( ( ph <-> ps ) -> ( ps -> ph ) )
12 11 imim2i 
 |-  ( ( x = A -> ( ph <-> ps ) ) -> ( x = A -> ( ps -> ph ) ) )
13 12 com23 
 |-  ( ( x = A -> ( ph <-> ps ) ) -> ( ps -> ( x = A -> ph ) ) )
14 13 alimi 
 |-  ( A. x ( x = A -> ( ph <-> ps ) ) -> A. x ( ps -> ( x = A -> ph ) ) )
15 14 3ad2ant2 
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> A. x ( ps -> ( x = A -> ph ) ) )
16 19.21t 
 |-  ( F/ x ps -> ( A. x ( ps -> ( x = A -> ph ) ) <-> ( ps -> A. x ( x = A -> ph ) ) ) )
17 16 3ad2ant1 
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( ps -> ( x = A -> ph ) ) <-> ( ps -> A. x ( x = A -> ph ) ) ) )
18 15 17 mpbid 
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( ps -> A. x ( x = A -> ph ) ) )
19 10 18 impbid 
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) <-> ps ) )