Theorem elrab 2976

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1398   e. wcel 2205   {crab 2526

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rab 2531  df-v 2817

This theorem is referenced by:  elrab3  2977  elrabd  2978  elrab2  2979  ralrab  2981  rexrab  2983  rabsnt  3771  unimax  3953  ssintub  3972  intminss  3979  exmidexmid  4314  exmidsssnc  4321  rabxfrd  4595  ordtri2or2exmidlem  4653  onsucelsucexmidlem1  4655  sefvex  5696  ssimaex  5743  acexmidlem2  6055  elsuppfng  6455  elsuppfn  6456  elpmg  6911  ssfilem  7143  ssfilemd  7145  diffitest  7157  inffiexmid  7179  2omap  7282  supubti  7303  suplubti  7304  ctssexmid  7454  sspw1or2  7508  exmidonfinlem  7509  finacn  7524  cc4f  7599  cc4n  7601  acnccim  7602  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemub  8054  nnindnn  8224  negf1o  8672  apsscn  8938  sup3exmid  9248  nnind  9270  peano2uz2  9703  peano5uzti  9704  dfuzi  9706  uzind  9707  uzind3  9709  eluz1  9875  uzind4  9938  supinfneg  9945  infsupneg  9946  eqreznegel  9964  elixx1  10249  elioo2  10273  elfz1  10366  zsupcl  10613  infssuzex  10615  infssuzcldc  10617  expcl2lemap  10937  expclzaplem  10949  expclzap  10950  expap0i  10957  expge0  10961  expge1  10962  hashennnuni  11167  hashfibclem  11231  wrdmap  11281  shftf  11540  reccn2ap  12023  dvdsdivcl  12561  divalgmod  12638  bitsval  12654  bitsfzolem  12665  bezoutlemsup  12730  dfgcd2  12735  uzwodc  12758  nnwosdc  12760  nninfctlemfo  12761  lcmgcdlem  12799  1nprm  12836  1idssfct  12837  isprm2  12839  phicl2  12936  hashdvds  12943  dvdsfi  12961  phisum  12963  odzval  12964  odzcllem  12965  odzdvds  12968  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemiex  13188  ballotfilemimin  13193  ballotfilemfrcn0  13217  ballotfilemirc  13219  ballotfilem7  13223  oddennn  13227  evenennn  13228  znnen  13233  ennnfonelemg  13238  ennnfonelemom  13243  ismhm  13716  issubm  13727  issubmd  13729  grplinv  13805  issubg  13926  isnsg  13955  isrim0  14406  issubrng  14445  issubrg  14467  ringunitsap0  14532  drnguiap  14547  islssm  14631  islssmg  14632  cnfldui  14863  mplelbascoe  14973  istopon  15004  epttop  15081  iscld  15094  isnei  15135  neipsm  15145  iscn  15188  iscnp  15190  txdis1cn  15269  ishmeo  15295  ispsmet  15314  ismet  15335  isxmet  15336  elblps  15381  elbl  15382  xmetxpbl  15499  reopnap  15537  divcnap  15556  elcncf  15564  cdivcncfap  15595  cnopnap  15602  divcncfap  15605  maxcncf  15606  mincncf  15607  ellimc3apf  15651  limccoap  15669  dvlemap  15671  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvcnp2cntop  15690  dvaddxxbr  15692  dvmulxxbr  15693  dvcoapbr  15698  dvcjbr  15699  dvrecap  15704  dveflem  15717  pellexlem3  15973  dvdsppwf1o  15983  lgsfle1  16008  lgsle1  16014  lgsdirprm  16033  lgsne0  16037  lgsquadlem1  16076  lgsquadlem2  16077  uhgrm  16199  upgrm  16221  upgr1or2  16222  umgredg2en  16230  umgrbien  16231  uhgredgm  16257  edgupgren  16262  edgumgren  16263  edgusgren  16284  usgruspgrben  16307  ushgredgedg  16347  ushgredgedgloop  16349  isclwwlk  16515  isclwwlkng  16527  clwwlknon  16550  eupth2lemsfi  16599  konigsberglem1  16609  konigsberglem4  16612  pw1map  16895  subctctexmid  16900