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  16093  dvdsppwf1o  16103  lgsfle1  16128  lgsle1  16134  lgsdirprm  16153  lgsne0  16157  lgsquadlem1  16196  lgsquadlem2  16197  uhgrm  16319  upgrm  16341  upgr1or2  16342  umgredg2en  16350  umgrbien  16351  uhgredgm  16377  edgupgren  16382  edgumgren  16383  edgusgren  16404  usgruspgrben  16427  ushgredgedg  16467  ushgredgedgloop  16469  isclwwlk  16635  isclwwlkng  16647  clwwlknon  16670  eupth2lemsfi  16719  konigsberglem1  16729  konigsberglem4  16732  pw1map  17025  subctctexmid  17030  wexmiddiffilem  17043