Metamath Proof Explorer

Theorem elab3g

Description: Membership in a class abstraction, with a weaker antecedent than elabg . (Contributed by NM, 29-Aug-2006)

Ref Expression
Hypothesis elab3g.1 
|- ( x = A -> ( ph <-> ps ) )
Assertion elab3g 
|- ( ( ps -> A e. B ) -> ( A e. { x | ph } <-> ps ) )

Proof

Step Hyp Ref Expression
1 elab3g.1 
 |-  ( x = A -> ( ph <-> ps ) )
2 nfcv 
 |-  F/_ x A
3 nfv 
 |-  F/ x ps
4 2 3 1 elab3gf 
 |-  ( ( ps -> A e. B ) -> ( A e. { x | ph } <-> ps ) )