Theorem elrab3 2888

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 2887	. 2 |- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )
3	2	baib 915	1 |- ( A e. B -> ( A e. { x e. B | ph } <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1349   e. wcel 2142   {crab 2453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-rab 2458  df-v 2733

This theorem is referenced by:  unimax  3831  undifexmid  4180  frind  4338  ordtriexmidlem2  4505  ordtriexmid  4506  ontriexmidim  4507  ordtri2orexmid  4508  onsucelsucexmid  4515  0elsucexmid  4550  ordpwsucexmid  4555  ordtri2or2exmid  4556  ontri2orexmidim  4557  canth  5811  acexmidlema  5848  acexmidlemb  5849  isnumi  7163  genpelvl  7478  genpelvu  7479  cauappcvgprlemladdru  7622  cauappcvgprlem1  7625  caucvgprlem1  7645  sup3exmid  8877  supinfneg  9558  infsupneg  9559  supminfex  9560  ublbneg  9576  negm  9578  hashinfuni  10715  infssuzex  11908  gcddvds  11922  dvdslegcd  11923  bezoutlemsup  11968  uzwodc  11996  lcmval  12021  dvdslcm  12027  isprm2lem  12074