Theorem elrab3 2977

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1398   e. wcel 2205   {crab 2526

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rab 2531  df-v 2817

This theorem is referenced by:  unimax  3953  undifexmid  4311  frind  4478  ordtriexmidlem2  4647  ordtriexmid  4648  ontriexmidim  4649  ordtri2orexmid  4650  onsucelsucexmid  4657  0elsucexmid  4692  ordpwsucexmid  4697  ordtri2or2exmid  4698  ontri2orexmidim  4699  canth  6009  acexmidlema  6049  acexmidlemb  6050  isnumi  7491  genpelvl  7843  genpelvu  7844  cauappcvgprlemladdru  7987  cauappcvgprlem1  7990  caucvgprlem1  8010  sup3exmid  9248  supinfneg  9945  infsupneg  9946  supminfex  9947  ublbneg  9963  negm  9965  infssuzex  10615  hashinfuni  11165  gcddvds  12684  dvdslegcd  12685  bezoutlemsup  12730  uzwodc  12758  lcmval  12785  dvdslcm  12791  isprm2lem  12838  eupth2lem3lem3fi  16591  eupth2lem3lem6fi  16592  eupth2lem3lem4fi  16594