Metamath Proof Explorer


Theorem ceqsralvOLD

Description: Obsolete version of ceqsalv as of 8-Sep-2024. (Contributed by NM, 21-Jun-2013) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis ceqsralv.2
|- ( x = A -> ( ph <-> ps ) )
Assertion ceqsralvOLD
|- ( A e. B -> ( A. x e. B ( x = A -> ph ) <-> ps ) )

Proof

Step Hyp Ref Expression
1 ceqsralv.2
 |-  ( x = A -> ( ph <-> ps ) )
2 nfv
 |-  F/ x ps
3 1 ax-gen
 |-  A. x ( x = A -> ( ph <-> ps ) )
4 ceqsralt
 |-  ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) /\ A e. B ) -> ( A. x e. B ( x = A -> ph ) <-> ps ) )
5 2 3 4 mp3an12
 |-  ( A e. B -> ( A. x e. B ( x = A -> ph ) <-> ps ) )