Theorem elrab 2929

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 2348	. 2 |- F/_ x A
2		nfcv 2348	. 2 |- F/_ x B
3		nfv 1551	. 2 |- F/ x ps
4		elrab.1	. 2 |- ( x = A -> ( ph <-> ps ) )
5	1, 2, 3, 4	elrabf 2927	1 |- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1373   e. wcel 2176   {crab 2488

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rab 2493  df-v 2774

This theorem is referenced by:  elrab3  2930  elrabd  2931  elrab2  2932  ralrab  2934  rexrab  2936  rabsnt  3708  unimax  3884  ssintub  3903  intminss  3910  exmidexmid  4240  exmidsssnc  4247  rabxfrd  4516  ordtri2or2exmidlem  4574  onsucelsucexmidlem1  4576  sefvex  5597  ssimaex  5640  acexmidlem2  5941  elpmg  6751  ssfilem  6972  diffitest  6984  inffiexmid  7003  supubti  7101  suplubti  7102  ctssexmid  7252  exmidonfinlem  7301  finacn  7316  cc4f  7381  cc4n  7383  acnccim  7384  caucvgprlemladdfu  7790  caucvgprlemladdrl  7791  suplocexprlemmu  7831  suplocexprlemru  7832  suplocexprlemdisj  7833  suplocexprlemub  7836  nnindnn  8006  negf1o  8454  apsscn  8720  sup3exmid  9030  nnind  9052  peano2uz2  9480  peano5uzti  9481  dfuzi  9483  uzind  9484  uzind3  9486  eluz1  9652  uzind4  9709  supinfneg  9716  infsupneg  9717  eqreznegel  9735  elixx1  10019  elioo2  10043  elfz1  10135  zsupcl  10374  infssuzex  10376  infssuzcldc  10378  expcl2lemap  10696  expclzaplem  10708  expclzap  10709  expap0i  10716  expge0  10720  expge1  10721  hashennnuni  10924  wrdmap  11025  shftf  11141  reccn2ap  11624  dvdsdivcl  12161  divalgmod  12238  bitsval  12254  bitsfzolem  12265  bezoutlemsup  12330  dfgcd2  12335  uzwodc  12358  nnwosdc  12360  nninfctlemfo  12361  lcmgcdlem  12399  1nprm  12436  1idssfct  12437  isprm2  12439  phicl2  12536  hashdvds  12543  dvdsfi  12561  phisum  12563  odzval  12564  odzcllem  12565  odzdvds  12568  oddennn  12763  evenennn  12764  znnen  12769  ennnfonelemg  12774  ennnfonelemom  12779  ismhm  13293  issubm  13304  issubmd  13306  grplinv  13382  issubg  13509  isnsg  13538  isrim0  13923  issubrng  13961  issubrg  13983  islssm  14119  islssmg  14120  cnfldui  14351  mplelbascoe  14454  istopon  14485  epttop  14562  iscld  14575  isnei  14616  neipsm  14626  iscn  14669  iscnp  14671  txdis1cn  14750  ishmeo  14776  ispsmet  14795  ismet  14816  isxmet  14817  elblps  14862  elbl  14863  xmetxpbl  14980  reopnap  15018  divcnap  15037  elcncf  15045  cdivcncfap  15076  cnopnap  15083  divcncfap  15086  maxcncf  15087  mincncf  15088  ellimc3apf  15132  limccoap  15150  dvlemap  15152  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvcnp2cntop  15171  dvaddxxbr  15173  dvmulxxbr  15174  dvcoapbr  15179  dvcjbr  15180  dvrecap  15185  dveflem  15198  dvdsppwf1o  15461  lgsfle1  15486  lgsle1  15492  lgsdirprm  15511  lgsne0  15515  lgsquadlem1  15554  lgsquadlem2  15555  2omap  15936  subctctexmid  15941