Theorem elrab 2886

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

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1348   e. wcel 2141   {crab 2452

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rab 2457  df-v 2732

This theorem is referenced by:  elrab3  2887  elrabd  2888  elrab2  2889  ralrab  2891  rexrab  2893  rabsnt  3658  unimax  3830  ssintub  3849  intminss  3856  exmidexmid  4182  exmidsssnc  4189  rabxfrd  4454  ordtri2or2exmidlem  4510  onsucelsucexmidlem1  4512  sefvex  5517  ssimaex  5557  acexmidlem2  5850  elpmg  6642  ssfilem  6853  diffitest  6865  inffiexmid  6884  supubti  6976  suplubti  6977  ctssexmid  7126  exmidonfinlem  7170  cc4f  7231  cc4n  7233  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  suplocexprlemmu  7680  suplocexprlemru  7681  suplocexprlemdisj  7682  suplocexprlemub  7685  nnindnn  7855  negf1o  8301  apsscn  8566  sup3exmid  8873  nnind  8894  peano2uz2  9319  peano5uzti  9320  dfuzi  9322  uzind  9323  uzind3  9325  eluz1  9491  uzind4  9547  supinfneg  9554  infsupneg  9555  eqreznegel  9573  elixx1  9854  elioo2  9878  elfz1  9970  expcl2lemap  10488  expclzaplem  10500  expclzap  10501  expap0i  10508  expge0  10512  expge1  10513  hashennnuni  10713  shftf  10794  reccn2ap  11276  dvdsdivcl  11810  divalgmod  11886  zsupcl  11902  infssuzex  11904  infssuzcldc  11906  bezoutlemsup  11964  dfgcd2  11969  uzwodc  11992  nnwosdc  11994  lcmcllem  12021  lcmledvds  12024  lcmgcdlem  12031  1nprm  12068  1idssfct  12069  isprm2  12071  phicl2  12168  hashdvds  12175  phisum  12194  odzval  12195  odzcllem  12196  odzdvds  12199  oddennn  12347  evenennn  12348  znnen  12353  ennnfonelemg  12358  ennnfonelemom  12363  ismhm  12685  issubm  12695  issubmd  12696  grplinv  12752  istopon  12805  epttop  12884  iscld  12897  isnei  12938  neipsm  12948  iscn  12991  iscnp  12993  txdis1cn  13072  ishmeo  13098  ispsmet  13117  ismet  13138  isxmet  13139  elblps  13184  elbl  13185  xmetxpbl  13302  reopnap  13332  divcnap  13349  elcncf  13354  cdivcncfap  13381  cnopnap  13388  ellimc3apf  13423  limccoap  13441  dvlemap  13443  dvidlemap  13454  dvcnp2cntop  13457  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465  dvcjbr  13466  dvrecap  13471  dveflem  13481  lgsfle1  13704  lgsle1  13710  lgsdirprm  13729  lgsne0  13733  subctctexmid  14034