Theorem elrab 2844

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

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1332   e. wcel 1481   {crab 2421

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rab 2426  df-v 2691

This theorem is referenced by:  elrab3  2845  elrabd  2846  elrab2  2847  ralrab  2849  rexrab  2851  rabsnt  3606  unimax  3778  ssintub  3797  intminss  3804  exmidexmid  4128  exmidsssnc  4134  rabxfrd  4398  ordtri2or2exmidlem  4449  onsucelsucexmidlem1  4451  sefvex  5450  ssimaex  5490  acexmidlem2  5779  elpmg  6566  ssfilem  6777  diffitest  6789  inffiexmid  6808  supubti  6894  suplubti  6895  ctssexmid  7032  exmidonfinlem  7066  cc4f  7101  cc4n  7103  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  suplocexprlemmu  7550  suplocexprlemru  7551  suplocexprlemdisj  7552  suplocexprlemub  7555  nnindnn  7725  negf1o  8168  apsscn  8433  sup3exmid  8739  nnind  8760  peano2uz2  9182  peano5uzti  9183  dfuzi  9185  uzind  9186  uzind3  9188  eluz1  9354  uzind4  9410  supinfneg  9417  infsupneg  9418  eqreznegel  9433  elixx1  9710  elioo2  9734  elfz1  9826  expcl2lemap  10336  expclzaplem  10348  expclzap  10349  expap0i  10356  expge0  10360  expge1  10361  hashennnuni  10557  shftf  10634  reccn2ap  11114  dvdsdivcl  11584  divalgmod  11660  zsupcl  11676  infssuzex  11678  infssuzcldc  11680  bezoutlemsup  11733  dfgcd2  11738  lcmcllem  11784  lcmledvds  11787  lcmgcdlem  11794  1nprm  11831  1idssfct  11832  isprm2  11834  phicl2  11926  hashdvds  11933  oddennn  11941  evenennn  11942  znnen  11947  ennnfonelemg  11952  ennnfonelemom  11957  istopon  12219  epttop  12298  iscld  12311  isnei  12352  neipsm  12362  iscn  12405  iscnp  12407  txdis1cn  12486  ishmeo  12512  ispsmet  12531  ismet  12552  isxmet  12553  elblps  12598  elbl  12599  xmetxpbl  12716  reopnap  12746  divcnap  12763  elcncf  12768  cdivcncfap  12795  cnopnap  12802  ellimc3apf  12837  limccoap  12855  dvlemap  12857  dvidlemap  12868  dvcnp2cntop  12871  dvaddxxbr  12873  dvmulxxbr  12874  dvcoapbr  12879  dvcjbr  12880  dvrecap  12885  dveflem  12895  subctctexmid  13369