Metamath Proof Explorer

Theorem ceqsralv

Description: Restricted quantifier version of ceqsalv . (Contributed by NM, 21-Jun-2013)

Ref Expression
Hypothesis ceqsralv.2 
|- ( x = A -> ( ph <-> ps ) )
Assertion ceqsralv 
|- ( 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 ) )