This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ceqsalgALT

Description: Alternate proof of ceqsalg , not using ceqsalt . (Contributed by NM, 29-Oct-2003) (Proof shortened by Andrew Salmon, 8-Jun-2011) (Revised by BJ, 29-Sep-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses ceqsalg.1 
|- F/ x ps
ceqsalg.2 
|- ( x = A -> ( ph <-> ps ) )
Assertion ceqsalgALT 
|- ( A e. V -> ( A. x ( x = A -> ph ) <-> ps ) )

Proof

Step Hyp Ref Expression
1 ceqsalg.1 
 |-  F/ x ps
2 ceqsalg.2 
 |-  ( x = A -> ( ph <-> ps ) )
3 elisset 
 |-  ( A e. V -> E. x x = A )
4 nfa1 
 |-  F/ x A. x ( x = A -> ph )
5 2 biimpd 
 |-  ( x = A -> ( ph -> ps ) )
6 5 a2i 
 |-  ( ( x = A -> ph ) -> ( x = A -> ps ) )
7 6 sps 
 |-  ( A. x ( x = A -> ph ) -> ( x = A -> ps ) )
8 4 1 7 exlimd 
 |-  ( A. x ( x = A -> ph ) -> ( E. x x = A -> ps ) )
9 3 8 syl5com 
 |-  ( A e. V -> ( A. x ( x = A -> ph ) -> ps ) )
10 2 biimprcd 
 |-  ( ps -> ( x = A -> ph ) )
11 1 10 alrimi 
 |-  ( ps -> A. x ( x = A -> ph ) )
12 9 11 impbid1 
 |-  ( A e. V -> ( A. x ( x = A -> ph ) <-> ps ) )