Theorem elrab3 2983

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 5-Oct-2006.)

Hypothesis

Ref	Expression
elrab.1	|- ( x = A -> ( ph <-> ps ) )

Assertion

Ref	Expression
elrab3	|- ( A e. B -> ( A e. { x e. B | ph } <-> ps ) )

Distinct variable groups:   ps, x   x, A   x, B

Allowed substitution hint:   ph( x)

Proof of Theorem elrab3

Step	Hyp	Ref	Expression
1		elrab.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
2	1	elrab 2982	. 2 |- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )
3	2	baib 931	1 |- ( A e. B -> ( A e. { x e. B | ph } <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1402   e. wcel 2209   {crab 2532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-v 2823

This theorem is referenced by:  unimax  3964  undifexmid  4325  frind  4492  ordtriexmidlem2  4662  ordtriexmid  4663  ontriexmidim  4664  ordtri2orexmid  4665  onsucelsucexmid  4672  0elsucexmid  4707  ordpwsucexmid  4712  ordtri2or2exmid  4713  ontri2orexmidim  4714  canth  6026  acexmidlema  6066  acexmidlemb  6067  isnumi  7517  genpelvl  7869  genpelvu  7870  cauappcvgprlemladdru  8013  cauappcvgprlem1  8016  caucvgprlem1  8036  sup3exmid  9277  supinfneg  9974  infsupneg  9975  supminfex  9976  ublbneg  9992  negm  9994  infssuzex  10644  hashinfuni  11194  gcddvds  12718  dvdslegcd  12719  bezoutlemsup  12764  uzwodc  12792  lcmval  12819  dvdslcm  12825  isprm2lem  12872  eupth2lem3lem3fi  16625  eupth2lem3lem6fi  16626  eupth2lem3lem4fi  16628