Theorem elrab 2975

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 2973	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  2976  elrabd  2977  elrab2  2978  ralrab  2980  rexrab  2982  rabsnt  3768  unimax  3950  ssintub  3969  intminss  3976  exmidexmid  4311  exmidsssnc  4318  rabxfrd  4592  ordtri2or2exmidlem  4650  onsucelsucexmidlem1  4652  sefvex  5693  ssimaex  5740  acexmidlem2  6049  elsuppfng  6444  elsuppfn  6445  elpmg  6900  ssfilem  7132  ssfilemd  7134  diffitest  7146  inffiexmid  7168  2omap  7271  supubti  7292  suplubti  7293  ctssexmid  7443  sspw1or2  7497  exmidonfinlem  7498  finacn  7513  cc4f  7585  cc4n  7587  acnccim  7588  caucvgprlemladdfu  7994  caucvgprlemladdrl  7995  suplocexprlemmu  8035  suplocexprlemru  8036  suplocexprlemdisj  8037  suplocexprlemub  8040  nnindnn  8210  negf1o  8657  apsscn  8923  sup3exmid  9233  nnind  9255  peano2uz2  9688  peano5uzti  9689  dfuzi  9691  uzind  9692  uzind3  9694  eluz1  9860  uzind4  9923  supinfneg  9930  infsupneg  9931  eqreznegel  9949  elixx1  10233  elioo2  10257  elfz1  10350  zsupcl  10595  infssuzex  10597  infssuzcldc  10599  expcl2lemap  10917  expclzaplem  10929  expclzap  10930  expap0i  10937  expge0  10941  expge1  10942  hashennnuni  11146  hashfibclem  11210  wrdmap  11260  shftf  11519  reccn2ap  12002  dvdsdivcl  12540  divalgmod  12617  bitsval  12633  bitsfzolem  12644  bezoutlemsup  12709  dfgcd2  12714  uzwodc  12737  nnwosdc  12739  nninfctlemfo  12740  lcmgcdlem  12778  1nprm  12815  1idssfct  12816  isprm2  12818  phicl2  12915  hashdvds  12922  dvdsfi  12940  phisum  12942  odzval  12943  odzcllem  12944  odzdvds  12947  ballotfilemfc0  13153  ballotfilemfcc  13154  oddennn  13160  evenennn  13161  znnen  13166  ennnfonelemg  13171  ennnfonelemom  13176  ismhm  13691  issubm  13702  issubmd  13704  grplinv  13780  issubg  13907  isnsg  13936  isrim0  14323  issubrng  14361  issubrg  14383  islssm  14522  islssmg  14523  cnfldui  14754  mplelbascoe  14864  istopon  14895  epttop  14972  iscld  14985  isnei  15026  neipsm  15036  iscn  15079  iscnp  15081  txdis1cn  15160  ishmeo  15186  ispsmet  15205  ismet  15226  isxmet  15227  elblps  15272  elbl  15273  xmetxpbl  15390  reopnap  15428  divcnap  15447  elcncf  15455  cdivcncfap  15486  cnopnap  15493  divcncfap  15496  maxcncf  15497  mincncf  15498  ellimc3apf  15542  limccoap  15560  dvlemap  15562  dvidlemap  15573  dvidrelem  15574  dvidsslem  15575  dvcnp2cntop  15581  dvaddxxbr  15583  dvmulxxbr  15584  dvcoapbr  15589  dvcjbr  15590  dvrecap  15595  dveflem  15608  pellexlem3  15864  dvdsppwf1o  15874  lgsfle1  15899  lgsle1  15905  lgsdirprm  15924  lgsne0  15928  lgsquadlem1  15967  lgsquadlem2  15968  uhgrm  16090  upgrm  16112  upgr1or2  16113  umgredg2en  16121  umgrbien  16122  uhgredgm  16148  edgupgren  16153  edgumgren  16154  edgusgren  16175  usgruspgrben  16198  ushgredgedg  16238  ushgredgedgloop  16240  isclwwlk  16406  isclwwlkng  16418  clwwlknon  16441  eupth2lemsfi  16490  konigsberglem1  16500  konigsberglem4  16503  pw1map  16786  subctctexmid  16791