Theorem elrab3 2892

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353   e. wcel 2146   {crab 2457

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rab 2462  df-v 2737

This theorem is referenced by:  unimax  3839  undifexmid  4188  frind  4346  ordtriexmidlem2  4513  ordtriexmid  4514  ontriexmidim  4515  ordtri2orexmid  4516  onsucelsucexmid  4523  0elsucexmid  4558  ordpwsucexmid  4563  ordtri2or2exmid  4564  ontri2orexmidim  4565  canth  5819  acexmidlema  5856  acexmidlemb  5857  isnumi  7171  genpelvl  7486  genpelvu  7487  cauappcvgprlemladdru  7630  cauappcvgprlem1  7633  caucvgprlem1  7653  sup3exmid  8887  supinfneg  9568  infsupneg  9569  supminfex  9570  ublbneg  9586  negm  9588  hashinfuni  10725  infssuzex  11917  gcddvds  11931  dvdslegcd  11932  bezoutlemsup  11977  uzwodc  12005  lcmval  12030  dvdslcm  12036  isprm2lem  12083