Theorem elrab 2749

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.)

Hypothesis

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

Assertion

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

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

Allowed substitution hint:   ph( x)

Proof of Theorem elrab

Step	Hyp	Ref	Expression
1		nfcv 2219	. 2 |- F/_ x A
2		nfcv 2219	. 2 |- F/_ x B
3		nfv 1461	. 2 |- F/ x ps
4		elrab.1	. 2 |- ( x = A -> ( ph <-> ps ) )
5	1, 2, 3, 4	elrabf 2747	1 |- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   = wceq 1284   e. wcel 1433   {crab 2352

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-rab 2357  df-v 2603

This theorem is referenced by:  elrab3  2750  elrab2  2751  ralrab  2753  rexrab  2755  rabsnt  3467  unimax  3635  ssintub  3654  intminss  3661  rabxfrd  4219  ordtri2or2exmidlem  4269  onsucelsucexmidlem1  4271  sefvex  5216  ssimaex  5255  acexmidlem2  5529  ssfilem  6360  diffitest  6371  supubti  6412  suplubti  6413  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  nnindnn  7059  negf1o  7486  nnind  8055  peano2uz2  8454  peano5uzti  8455  dfuzi  8457  uzind  8458  uzind3  8460  eluz1  8623  uzind4  8676  supinfneg  8683  infsupneg  8684  eqreznegel  8699  elixx1  8920  elioo2  8944  elfz1  9034  serige0  9473  expcl2lemap  9488  expclzaplem  9500  expclzap  9501  expap0i  9508  expge0  9512  expge1  9513  shftf  9718  dvdsdivcl  10250  divalgmod  10327  zsupcl  10343  infssuzex  10345  infssuzcldc  10347  bezoutlemsup  10398  dfgcd2  10403  lcmcllem  10449  lcmledvds  10452  lcmgcdlem  10459  1nprm  10496  1idssfct  10497  isprm2  10499