Theorem elrab 2959

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1395   e. wcel 2200   {crab 2512

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-v 2801

This theorem is referenced by:  elrab3  2960  elrabd  2961  elrab2  2962  ralrab  2964  rexrab  2966  rabsnt  3741  unimax  3922  ssintub  3941  intminss  3948  exmidexmid  4280  exmidsssnc  4287  rabxfrd  4560  ordtri2or2exmidlem  4618  onsucelsucexmidlem1  4620  sefvex  5648  ssimaex  5695  acexmidlem2  5998  elpmg  6811  ssfilem  7037  diffitest  7049  inffiexmid  7068  supubti  7166  suplubti  7167  ctssexmid  7317  exmidonfinlem  7371  finacn  7386  cc4f  7455  cc4n  7457  acnccim  7458  caucvgprlemladdfu  7864  caucvgprlemladdrl  7865  suplocexprlemmu  7905  suplocexprlemru  7906  suplocexprlemdisj  7907  suplocexprlemub  7910  nnindnn  8080  negf1o  8528  apsscn  8794  sup3exmid  9104  nnind  9126  peano2uz2  9554  peano5uzti  9555  dfuzi  9557  uzind  9558  uzind3  9560  eluz1  9726  uzind4  9783  supinfneg  9790  infsupneg  9791  eqreznegel  9809  elixx1  10093  elioo2  10117  elfz1  10209  zsupcl  10451  infssuzex  10453  infssuzcldc  10455  expcl2lemap  10773  expclzaplem  10785  expclzap  10786  expap0i  10793  expge0  10797  expge1  10798  hashennnuni  11001  wrdmap  11103  shftf  11341  reccn2ap  11824  dvdsdivcl  12361  divalgmod  12438  bitsval  12454  bitsfzolem  12465  bezoutlemsup  12530  dfgcd2  12535  uzwodc  12558  nnwosdc  12560  nninfctlemfo  12561  lcmgcdlem  12599  1nprm  12636  1idssfct  12637  isprm2  12639  phicl2  12736  hashdvds  12743  dvdsfi  12761  phisum  12763  odzval  12764  odzcllem  12765  odzdvds  12768  oddennn  12963  evenennn  12964  znnen  12969  ennnfonelemg  12974  ennnfonelemom  12979  ismhm  13494  issubm  13505  issubmd  13507  grplinv  13583  issubg  13710  isnsg  13739  isrim0  14125  issubrng  14163  issubrg  14185  islssm  14321  islssmg  14322  cnfldui  14553  mplelbascoe  14656  istopon  14687  epttop  14764  iscld  14777  isnei  14818  neipsm  14828  iscn  14871  iscnp  14873  txdis1cn  14952  ishmeo  14978  ispsmet  14997  ismet  15018  isxmet  15019  elblps  15064  elbl  15065  xmetxpbl  15182  reopnap  15220  divcnap  15239  elcncf  15247  cdivcncfap  15278  cnopnap  15285  divcncfap  15288  maxcncf  15289  mincncf  15290  ellimc3apf  15334  limccoap  15352  dvlemap  15354  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367  dvcnp2cntop  15373  dvaddxxbr  15375  dvmulxxbr  15376  dvcoapbr  15381  dvcjbr  15382  dvrecap  15387  dveflem  15400  dvdsppwf1o  15663  lgsfle1  15688  lgsle1  15694  lgsdirprm  15713  lgsne0  15717  lgsquadlem1  15756  lgsquadlem2  15757  uhgrm  15878  upgrm  15900  upgr1or2  15901  umgredg2en  15909  umgrbien  15910  uhgredgm  15934  edgupgren  15939  edgumgren  15940  edgusgren  15961  usgruspgrben  15984  ushgredgedg  16024  ushgredgedgloop  16026  2omap  16359  pw1map  16361  subctctexmid  16366