Theorem elrab 2982

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   e. wcel 2209   {crab 2532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-v 2823

This theorem is used by:  elrab3  2983  elrabd  2984  elrab2  2985  ralrab  2987  rexrab  2989  rabsnt  3786  unimax  3969  ssintub  3988  intminss  3995  exmidexmid  4333  exmidsssnc  4340  rabxfrd  4615  ordtri2or2exmidlem  4673  onsucelsucexmidlem1  4675  sefvex  5716  ssimaex  5764  acexmidlem2  6082  elsuppfng  6482  elsuppfn  6483  elpmg  6938  ssfilem  7177  ssfilemd  7179  diffitest  7191  inffiexmid  7213  2omap  7318  supubti  7339  suplubti  7340  ctssexmid  7490  sspw1or2  7544  exmidonfinlem  7545  finacn  7560  cc4f  7635  cc4n  7637  acnccim  7638  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemub  8090  nnindnn  8260  negf1o  8710  apsscn  8977  sup3exmid  9289  nnind  9322  peano2uz2  9757  peano5uzti  9758  dfuzi  9760  uzind  9761  uzind3  9763  eluz1  9934  uzind4  9997  supinfneg  10004  infsupneg  10005  eqreznegel  10023  elixx1  10309  elioo2  10333  elfz1  10426  zsupcl  10674  infssuzex  10676  infssuzcldc  10678  expcl2lemap  11001  expclzaplem  11013  expclzap  11014  expap0i  11021  expge0  11025  expge1  11026  hashennnuni  11232  hashfibclem  11296  wrdmap  11350  shftf  11609  reccn2ap  12095  dvdsdivcl  12633  divalgmod  12710  bitsval  12726  bitsfzolem  12737  bezoutlemsup  12802  dfgcd2  12807  uzwodc  12830  nnwosdc  12832  nninfctlemfo  12833  lcmgcdlem  12871  1nprm  12908  1idssfct  12909  isprm2  12911  phicl2  13012  hashdvds  13019  dvdsfi  13037  phisum  13039  odzval  13040  odzcllem  13041  odzdvds  13044  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemiex  13293  ballotfilemimin  13298  ballotfilemfrcn0  13322  ballotfilemirc  13324  ballotfilem7  13328  oddennn  13332  evenennn  13333  znnen  13338  ennnfonelemg  13343  ennnfonelemom  13348  ismhm  13817  issubm  13828  issubmd  13830  grplinv  13904  issubg  14025  isnsg  14054  isrim0  14517  issubrng  14556  issubrg  14578  ringunitsap0  14643  drnguiap  14658  islssm  14743  islssmg  14744  cnfldui  14973  mplelbascoe  15132  istopon  15163  epttop  15240  iscld  15253  isnei  15294  neipsm  15304  iscn  15347  iscnp  15349  txdis1cn  15428  ishmeo  15454  ispsmet  15473  ismet  15494  isxmet  15495  elblps  15540  elbl  15541  xmetxpbl  15658  reopnap  15696  divcnap  15715  elcncf  15723  cdivcncfap  15754  cnopnap  15761  divcncfap  15764  maxcncf  15765  mincncf  15766  ellimc3apf  15810  limccoap  15828  dvlemap  15830  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvcnp2cntop  15849  dvaddxxbr  15851  dvmulxxbr  15852  dvcoapbr  15857  dvcjbr  15858  dvrecap  15863  dveflem  15876  pellexlem3  16150  prmdvdsfi  16159  dvdsppwf1o  16184  ppiqub  16194  lgsfle1  16226  lgsle1  16232  lgsdirprm  16251  lgsne0  16255  lgsquadlem1  16294  lgsquadlem2  16295  uhgrm  16417  upgrm  16439  upgr1or2  16440  umgredg2en  16448  umgrbien  16449  uhgredgm  16475  edgupgren  16480  edgumgren  16481  edgusgren  16502  usgruspgrben  16525  ushgredgedg  16565  ushgredgedgloop  16567  isclwwlk  16733  isclwwlkng  16745  clwwlknon  16768  eupth2lemsfi  16817  konigsberglem1  16827  konigsberglem4  16830  pw1map  17123  subctctexmid  17128  wexmiddiffilem  17141