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  8709  apsscn  8975  sup3exmid  9287  nnind  9320  peano2uz2  9753  peano5uzti  9754  dfuzi  9756  uzind  9757  uzind3  9759  eluz1  9925  uzind4  9988  supinfneg  9995  infsupneg  9996  eqreznegel  10014  elixx1  10299  elioo2  10323  elfz1  10416  zsupcl  10664  infssuzex  10666  infssuzcldc  10668  expcl2lemap  10988  expclzaplem  11000  expclzap  11001  expap0i  11008  expge0  11012  expge1  11013  hashennnuni  11218  hashfibclem  11282  wrdmap  11336  shftf  11595  reccn2ap  12079  dvdsdivcl  12617  divalgmod  12694  bitsval  12710  bitsfzolem  12721  bezoutlemsup  12786  dfgcd2  12791  uzwodc  12814  nnwosdc  12816  nninfctlemfo  12817  lcmgcdlem  12855  1nprm  12892  1idssfct  12893  isprm2  12895  phicl2  12992  hashdvds  12999  dvdsfi  13017  phisum  13019  odzval  13020  odzcllem  13021  odzdvds  13024  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemiex  13244  ballotfilemimin  13249  ballotfilemfrcn0  13273  ballotfilemirc  13275  ballotfilem7  13279  oddennn  13283  evenennn  13284  znnen  13289  ennnfonelemg  13294  ennnfonelemom  13299  ismhm  13768  issubm  13779  issubmd  13781  grplinv  13855  issubg  13976  isnsg  14005  isrim0  14468  issubrng  14507  issubrg  14529  ringunitsap0  14594  drnguiap  14609  islssm  14694  islssmg  14695  cnfldui  14924  mplelbascoe  15083  istopon  15114  epttop  15191  iscld  15204  isnei  15245  neipsm  15255  iscn  15298  iscnp  15300  txdis1cn  15379  ishmeo  15405  ispsmet  15424  ismet  15445  isxmet  15446  elblps  15491  elbl  15492  xmetxpbl  15609  reopnap  15647  divcnap  15666  elcncf  15674  cdivcncfap  15705  cnopnap  15712  divcncfap  15715  maxcncf  15716  mincncf  15717  ellimc3apf  15761  limccoap  15779  dvlemap  15781  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvcnp2cntop  15800  dvaddxxbr  15802  dvmulxxbr  15803  dvcoapbr  15808  dvcjbr  15809  dvrecap  15814  dveflem  15827  pellexlem3  16097  dvdsppwf1o  16107  lgsfle1  16132  lgsle1  16138  lgsdirprm  16157  lgsne0  16161  lgsquadlem1  16200  lgsquadlem2  16201  uhgrm  16323  upgrm  16345  upgr1or2  16346  umgredg2en  16354  umgrbien  16355  uhgredgm  16381  edgupgren  16386  edgumgren  16387  edgusgren  16408  usgruspgrben  16431  ushgredgedg  16471  ushgredgedgloop  16473  isclwwlk  16639  isclwwlkng  16651  clwwlknon  16674  eupth2lemsfi  16723  konigsberglem1  16733  konigsberglem4  16736  pw1map  17029  subctctexmid  17034  wexmiddiffilem  17047