Theorem elrab 2929

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1373   e. wcel 2176   {crab 2488

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rab 2493  df-v 2774

This theorem is referenced by:  elrab3  2930  elrabd  2931  elrab2  2932  ralrab  2934  rexrab  2936  rabsnt  3708  unimax  3884  ssintub  3903  intminss  3910  exmidexmid  4241  exmidsssnc  4248  rabxfrd  4517  ordtri2or2exmidlem  4575  onsucelsucexmidlem1  4577  sefvex  5599  ssimaex  5642  acexmidlem2  5943  elpmg  6753  ssfilem  6974  diffitest  6986  inffiexmid  7005  supubti  7103  suplubti  7104  ctssexmid  7254  exmidonfinlem  7303  finacn  7318  cc4f  7383  cc4n  7385  acnccim  7386  caucvgprlemladdfu  7792  caucvgprlemladdrl  7793  suplocexprlemmu  7833  suplocexprlemru  7834  suplocexprlemdisj  7835  suplocexprlemub  7838  nnindnn  8008  negf1o  8456  apsscn  8722  sup3exmid  9032  nnind  9054  peano2uz2  9482  peano5uzti  9483  dfuzi  9485  uzind  9486  uzind3  9488  eluz1  9654  uzind4  9711  supinfneg  9718  infsupneg  9719  eqreznegel  9737  elixx1  10021  elioo2  10045  elfz1  10137  zsupcl  10376  infssuzex  10378  infssuzcldc  10380  expcl2lemap  10698  expclzaplem  10710  expclzap  10711  expap0i  10718  expge0  10722  expge1  10723  hashennnuni  10926  wrdmap  11027  shftf  11174  reccn2ap  11657  dvdsdivcl  12194  divalgmod  12271  bitsval  12287  bitsfzolem  12298  bezoutlemsup  12363  dfgcd2  12368  uzwodc  12391  nnwosdc  12393  nninfctlemfo  12394  lcmgcdlem  12432  1nprm  12469  1idssfct  12470  isprm2  12472  phicl2  12569  hashdvds  12576  dvdsfi  12594  phisum  12596  odzval  12597  odzcllem  12598  odzdvds  12601  oddennn  12796  evenennn  12797  znnen  12802  ennnfonelemg  12807  ennnfonelemom  12812  ismhm  13326  issubm  13337  issubmd  13339  grplinv  13415  issubg  13542  isnsg  13571  isrim0  13956  issubrng  13994  issubrg  14016  islssm  14152  islssmg  14153  cnfldui  14384  mplelbascoe  14487  istopon  14518  epttop  14595  iscld  14608  isnei  14649  neipsm  14659  iscn  14702  iscnp  14704  txdis1cn  14783  ishmeo  14809  ispsmet  14828  ismet  14849  isxmet  14850  elblps  14895  elbl  14896  xmetxpbl  15013  reopnap  15051  divcnap  15070  elcncf  15078  cdivcncfap  15109  cnopnap  15116  divcncfap  15119  maxcncf  15120  mincncf  15121  ellimc3apf  15165  limccoap  15183  dvlemap  15185  dvidlemap  15196  dvidrelem  15197  dvidsslem  15198  dvcnp2cntop  15204  dvaddxxbr  15206  dvmulxxbr  15207  dvcoapbr  15212  dvcjbr  15213  dvrecap  15218  dveflem  15231  dvdsppwf1o  15494  lgsfle1  15519  lgsle1  15525  lgsdirprm  15544  lgsne0  15548  lgsquadlem1  15587  lgsquadlem2  15588  2omap  15969  subctctexmid  15974