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 biimp
 |-  ( ( ph <-> ps ) -> ( ph -> ps ) )
2 1 imim3i
 |-  ( ( x = A -> ( ph <-> ps ) ) -> ( ( x = A -> ph ) -> ( x = A -> ps ) ) )
3 2 al2imi
 |-  ( A. x ( x = A -> ( ph <-> ps ) ) -> ( A. x ( x = A -> ph ) -> A. x ( x = A -> ps ) ) )
4 elisset
 |-  ( A e. V -> E. x x = A )
5 19.23t
 |-  ( F/ x ps -> ( A. x ( x = A -> ps ) <-> ( E. x x = A -> ps ) ) )
6 5 biimpd
 |-  ( F/ x ps -> ( A. x ( x = A -> ps ) -> ( E. x x = A -> ps ) ) )
7 4 6 syl7
 |-  ( F/ x ps -> ( A. x ( x = A -> ps ) -> ( A e. V -> ps ) ) )
8 3 7 sylan9r
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( A. x ( x = A -> ph ) -> ( A e. V -> ps ) ) )
9 8 com23
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( A e. V -> ( A. x ( x = A -> ph ) -> ps ) ) )
10 9 3impia
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) -> ps ) )
11 ceqsal1t
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( ps -> A. x ( x = A -> ph ) ) )
12 11 3adant3
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( ps -> A. x ( x = A -> ph ) ) )
13 10 12 impbid
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. V ) -> ( A. x ( x = A -> ph ) <-> ps ) )