Theorem elrab 2963

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 2375	. 2 |- F/_ x A
2		nfcv 2375	. 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 2961	1 |- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )

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

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rab 2520  df-v 2805

This theorem is referenced by:  elrab3  2964  elrabd  2965  elrab2  2966  ralrab  2968  rexrab  2970  rabsnt  3750  unimax  3932  ssintub  3951  intminss  3958  exmidexmid  4292  exmidsssnc  4299  rabxfrd  4572  ordtri2or2exmidlem  4630  onsucelsucexmidlem1  4632  sefvex  5669  ssimaex  5716  acexmidlem2  6025  elsuppfng  6420  elsuppfn  6421  elpmg  6876  ssfilem  7105  ssfilemd  7107  diffitest  7119  inffiexmid  7141  supubti  7258  suplubti  7259  ctssexmid  7409  sspw1or2  7463  exmidonfinlem  7464  finacn  7479  cc4f  7548  cc4n  7550  acnccim  7551  caucvgprlemladdfu  7957  caucvgprlemladdrl  7958  suplocexprlemmu  7998  suplocexprlemru  7999  suplocexprlemdisj  8000  suplocexprlemub  8003  nnindnn  8173  negf1o  8620  apsscn  8886  sup3exmid  9196  nnind  9218  peano2uz2  9648  peano5uzti  9649  dfuzi  9651  uzind  9652  uzind3  9654  eluz1  9820  uzind4  9883  supinfneg  9890  infsupneg  9891  eqreznegel  9909  elixx1  10193  elioo2  10217  elfz1  10310  zsupcl  10554  infssuzex  10556  infssuzcldc  10558  expcl2lemap  10876  expclzaplem  10888  expclzap  10889  expap0i  10896  expge0  10900  expge1  10901  hashennnuni  11104  wrdmap  11211  shftf  11470  reccn2ap  11953  dvdsdivcl  12491  divalgmod  12568  bitsval  12584  bitsfzolem  12595  bezoutlemsup  12660  dfgcd2  12665  uzwodc  12688  nnwosdc  12690  nninfctlemfo  12691  lcmgcdlem  12729  1nprm  12766  1idssfct  12767  isprm2  12769  phicl2  12866  hashdvds  12873  dvdsfi  12891  phisum  12893  odzval  12894  odzcllem  12895  odzdvds  12898  oddennn  13093  evenennn  13094  znnen  13099  ennnfonelemg  13104  ennnfonelemom  13109  ismhm  13624  issubm  13635  issubmd  13637  grplinv  13713  issubg  13840  isnsg  13869  isrim0  14256  issubrng  14294  issubrg  14316  islssm  14453  islssmg  14454  cnfldui  14685  mplelbascoe  14793  istopon  14824  epttop  14901  iscld  14914  isnei  14955  neipsm  14965  iscn  15008  iscnp  15010  txdis1cn  15089  ishmeo  15115  ispsmet  15134  ismet  15155  isxmet  15156  elblps  15201  elbl  15202  xmetxpbl  15319  reopnap  15357  divcnap  15376  elcncf  15384  cdivcncfap  15415  cnopnap  15422  divcncfap  15425  maxcncf  15426  mincncf  15427  ellimc3apf  15471  limccoap  15489  dvlemap  15491  dvidlemap  15502  dvidrelem  15503  dvidsslem  15504  dvcnp2cntop  15510  dvaddxxbr  15512  dvmulxxbr  15513  dvcoapbr  15518  dvcjbr  15519  dvrecap  15524  dveflem  15537  pellexlem3  15793  dvdsppwf1o  15803  lgsfle1  15828  lgsle1  15834  lgsdirprm  15853  lgsne0  15857  lgsquadlem1  15896  lgsquadlem2  15897  uhgrm  16019  upgrm  16041  upgr1or2  16042  umgredg2en  16050  umgrbien  16051  uhgredgm  16077  edgupgren  16082  edgumgren  16083  edgusgren  16104  usgruspgrben  16127  ushgredgedg  16167  ushgredgedgloop  16169  isclwwlk  16335  isclwwlkng  16347  clwwlknon  16370  eupth2lemsfi  16419  konigsberglem1  16429  konigsberglem4  16432  2omap  16715  pw1map  16717  subctctexmid  16722