Theorem elrab 2882

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

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1343   e. wcel 2136   {crab 2448

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-rab 2453  df-v 2728

This theorem is referenced by:  elrab3  2883  elrabd  2884  elrab2  2885  ralrab  2887  rexrab  2889  rabsnt  3651  unimax  3823  ssintub  3842  intminss  3849  exmidexmid  4175  exmidsssnc  4182  rabxfrd  4447  ordtri2or2exmidlem  4503  onsucelsucexmidlem1  4505  sefvex  5507  ssimaex  5547  acexmidlem2  5839  elpmg  6630  ssfilem  6841  diffitest  6853  inffiexmid  6872  supubti  6964  suplubti  6965  ctssexmid  7114  exmidonfinlem  7149  cc4f  7210  cc4n  7212  caucvgprlemladdfu  7618  caucvgprlemladdrl  7619  suplocexprlemmu  7659  suplocexprlemru  7660  suplocexprlemdisj  7661  suplocexprlemub  7664  nnindnn  7834  negf1o  8280  apsscn  8545  sup3exmid  8852  nnind  8873  peano2uz2  9298  peano5uzti  9299  dfuzi  9301  uzind  9302  uzind3  9304  eluz1  9470  uzind4  9526  supinfneg  9533  infsupneg  9534  eqreznegel  9552  elixx1  9833  elioo2  9857  elfz1  9949  expcl2lemap  10467  expclzaplem  10479  expclzap  10480  expap0i  10487  expge0  10491  expge1  10492  hashennnuni  10692  shftf  10772  reccn2ap  11254  dvdsdivcl  11788  divalgmod  11864  zsupcl  11880  infssuzex  11882  infssuzcldc  11884  bezoutlemsup  11942  dfgcd2  11947  uzwodc  11970  nnwosdc  11972  lcmcllem  11999  lcmledvds  12002  lcmgcdlem  12009  1nprm  12046  1idssfct  12047  isprm2  12049  phicl2  12146  hashdvds  12153  phisum  12172  odzval  12173  odzcllem  12174  odzdvds  12177  oddennn  12325  evenennn  12326  znnen  12331  ennnfonelemg  12336  ennnfonelemom  12341  istopon  12651  epttop  12730  iscld  12743  isnei  12784  neipsm  12794  iscn  12837  iscnp  12839  txdis1cn  12918  ishmeo  12944  ispsmet  12963  ismet  12984  isxmet  12985  elblps  13030  elbl  13031  xmetxpbl  13148  reopnap  13178  divcnap  13195  elcncf  13200  cdivcncfap  13227  cnopnap  13234  ellimc3apf  13269  limccoap  13287  dvlemap  13289  dvidlemap  13300  dvcnp2cntop  13303  dvaddxxbr  13305  dvmulxxbr  13306  dvcoapbr  13311  dvcjbr  13312  dvrecap  13317  dveflem  13327  lgsfle1  13550  lgsle1  13556  lgsdirprm  13575  lgsne0  13579  subctctexmid  13881