Theorem elrab 2959

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1395   e. wcel 2200   {crab 2512

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-v 2801

This theorem is referenced by:  elrab3  2960  elrabd  2961  elrab2  2962  ralrab  2964  rexrab  2966  rabsnt  3741  unimax  3922  ssintub  3941  intminss  3948  exmidexmid  4280  exmidsssnc  4287  rabxfrd  4560  ordtri2or2exmidlem  4618  onsucelsucexmidlem1  4620  sefvex  5650  ssimaex  5697  acexmidlem2  6004  elpmg  6819  ssfilem  7045  diffitest  7057  inffiexmid  7079  supubti  7177  suplubti  7178  ctssexmid  7328  exmidonfinlem  7382  finacn  7397  cc4f  7466  cc4n  7468  acnccim  7469  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemub  7921  nnindnn  8091  negf1o  8539  apsscn  8805  sup3exmid  9115  nnind  9137  peano2uz2  9565  peano5uzti  9566  dfuzi  9568  uzind  9569  uzind3  9571  eluz1  9737  uzind4  9795  supinfneg  9802  infsupneg  9803  eqreznegel  9821  elixx1  10105  elioo2  10129  elfz1  10221  zsupcl  10463  infssuzex  10465  infssuzcldc  10467  expcl2lemap  10785  expclzaplem  10797  expclzap  10798  expap0i  10805  expge0  10809  expge1  10810  hashennnuni  11013  wrdmap  11116  shftf  11357  reccn2ap  11840  dvdsdivcl  12377  divalgmod  12454  bitsval  12470  bitsfzolem  12481  bezoutlemsup  12546  dfgcd2  12551  uzwodc  12574  nnwosdc  12576  nninfctlemfo  12577  lcmgcdlem  12615  1nprm  12652  1idssfct  12653  isprm2  12655  phicl2  12752  hashdvds  12759  dvdsfi  12777  phisum  12779  odzval  12780  odzcllem  12781  odzdvds  12784  oddennn  12979  evenennn  12980  znnen  12985  ennnfonelemg  12990  ennnfonelemom  12995  ismhm  13510  issubm  13521  issubmd  13523  grplinv  13599  issubg  13726  isnsg  13755  isrim0  14141  issubrng  14179  issubrg  14201  islssm  14337  islssmg  14338  cnfldui  14569  mplelbascoe  14672  istopon  14703  epttop  14780  iscld  14793  isnei  14834  neipsm  14844  iscn  14887  iscnp  14889  txdis1cn  14968  ishmeo  14994  ispsmet  15013  ismet  15034  isxmet  15035  elblps  15080  elbl  15081  xmetxpbl  15198  reopnap  15236  divcnap  15255  elcncf  15263  cdivcncfap  15294  cnopnap  15301  divcncfap  15304  maxcncf  15305  mincncf  15306  ellimc3apf  15350  limccoap  15368  dvlemap  15370  dvidlemap  15381  dvidrelem  15382  dvidsslem  15383  dvcnp2cntop  15389  dvaddxxbr  15391  dvmulxxbr  15392  dvcoapbr  15397  dvcjbr  15398  dvrecap  15403  dveflem  15416  dvdsppwf1o  15679  lgsfle1  15704  lgsle1  15710  lgsdirprm  15729  lgsne0  15733  lgsquadlem1  15772  lgsquadlem2  15773  uhgrm  15894  upgrm  15916  upgr1or2  15917  umgredg2en  15925  umgrbien  15926  uhgredgm  15950  edgupgren  15955  edgumgren  15956  edgusgren  15977  usgruspgrben  16000  ushgredgedg  16040  ushgredgedgloop  16042  isclwwlk  16137  isclwwlkng  16149  2omap  16446  pw1map  16448  subctctexmid  16453