Theorem elrab 2962

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1397   e. wcel 2202   {crab 2514

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rab 2519  df-v 2804

This theorem is referenced by:  elrab3  2963  elrabd  2964  elrab2  2965  ralrab  2967  rexrab  2969  rabsnt  3746  unimax  3927  ssintub  3946  intminss  3953  exmidexmid  4286  exmidsssnc  4293  rabxfrd  4566  ordtri2or2exmidlem  4624  onsucelsucexmidlem1  4626  sefvex  5660  ssimaex  5707  acexmidlem2  6015  elpmg  6833  ssfilem  7062  ssfilemd  7064  diffitest  7076  inffiexmid  7098  supubti  7198  suplubti  7199  ctssexmid  7349  sspw1or2  7403  exmidonfinlem  7404  finacn  7419  cc4f  7488  cc4n  7490  acnccim  7491  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemub  7943  nnindnn  8113  negf1o  8561  apsscn  8827  sup3exmid  9137  nnind  9159  peano2uz2  9587  peano5uzti  9588  dfuzi  9590  uzind  9591  uzind3  9593  eluz1  9759  uzind4  9822  supinfneg  9829  infsupneg  9830  eqreznegel  9848  elixx1  10132  elioo2  10156  elfz1  10248  zsupcl  10492  infssuzex  10494  infssuzcldc  10496  expcl2lemap  10814  expclzaplem  10826  expclzap  10827  expap0i  10834  expge0  10838  expge1  10839  hashennnuni  11042  wrdmap  11149  shftf  11408  reccn2ap  11891  dvdsdivcl  12429  divalgmod  12506  bitsval  12522  bitsfzolem  12533  bezoutlemsup  12598  dfgcd2  12603  uzwodc  12626  nnwosdc  12628  nninfctlemfo  12629  lcmgcdlem  12667  1nprm  12704  1idssfct  12705  isprm2  12707  phicl2  12804  hashdvds  12811  dvdsfi  12829  phisum  12831  odzval  12832  odzcllem  12833  odzdvds  12836  oddennn  13031  evenennn  13032  znnen  13037  ennnfonelemg  13042  ennnfonelemom  13047  ismhm  13562  issubm  13573  issubmd  13575  grplinv  13651  issubg  13778  isnsg  13807  isrim0  14194  issubrng  14232  issubrg  14254  islssm  14390  islssmg  14391  cnfldui  14622  mplelbascoe  14725  istopon  14756  epttop  14833  iscld  14846  isnei  14887  neipsm  14897  iscn  14940  iscnp  14942  txdis1cn  15021  ishmeo  15047  ispsmet  15066  ismet  15087  isxmet  15088  elblps  15133  elbl  15134  xmetxpbl  15251  reopnap  15289  divcnap  15308  elcncf  15316  cdivcncfap  15347  cnopnap  15354  divcncfap  15357  maxcncf  15358  mincncf  15359  ellimc3apf  15403  limccoap  15421  dvlemap  15423  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvcnp2cntop  15442  dvaddxxbr  15444  dvmulxxbr  15445  dvcoapbr  15450  dvcjbr  15451  dvrecap  15456  dveflem  15469  dvdsppwf1o  15732  lgsfle1  15757  lgsle1  15763  lgsdirprm  15782  lgsne0  15786  lgsquadlem1  15825  lgsquadlem2  15826  uhgrm  15948  upgrm  15970  upgr1or2  15971  umgredg2en  15979  umgrbien  15980  uhgredgm  16006  edgupgren  16011  edgumgren  16012  edgusgren  16033  usgruspgrben  16056  ushgredgedg  16096  ushgredgedgloop  16098  isclwwlk  16264  isclwwlkng  16276  clwwlknon  16299  eupth2lemsfi  16348  konigsberglem1  16358  konigsberglem4  16361  2omap  16645  pw1map  16647  subctctexmid  16652