Theorem elrab 2917

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1364   e. wcel 2164   {crab 2476

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rab 2481  df-v 2762

This theorem is referenced by:  elrab3  2918  elrabd  2919  elrab2  2920  ralrab  2922  rexrab  2924  rabsnt  3694  unimax  3870  ssintub  3889  intminss  3896  exmidexmid  4226  exmidsssnc  4233  rabxfrd  4501  ordtri2or2exmidlem  4559  onsucelsucexmidlem1  4561  sefvex  5576  ssimaex  5619  acexmidlem2  5916  elpmg  6720  ssfilem  6933  diffitest  6945  inffiexmid  6964  supubti  7060  suplubti  7061  ctssexmid  7211  exmidonfinlem  7255  cc4f  7331  cc4n  7333  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  suplocexprlemmu  7780  suplocexprlemru  7781  suplocexprlemdisj  7782  suplocexprlemub  7785  nnindnn  7955  negf1o  8403  apsscn  8668  sup3exmid  8978  nnind  9000  peano2uz2  9427  peano5uzti  9428  dfuzi  9430  uzind  9431  uzind3  9433  eluz1  9599  uzind4  9656  supinfneg  9663  infsupneg  9664  eqreznegel  9682  elixx1  9966  elioo2  9990  elfz1  10082  expcl2lemap  10625  expclzaplem  10637  expclzap  10638  expap0i  10645  expge0  10649  expge1  10650  hashennnuni  10853  wrdmap  10948  shftf  10977  reccn2ap  11459  dvdsdivcl  11995  divalgmod  12071  zsupcl  12087  infssuzex  12089  infssuzcldc  12091  bezoutlemsup  12149  dfgcd2  12154  uzwodc  12177  nnwosdc  12179  nninfctlemfo  12180  lcmgcdlem  12218  1nprm  12255  1idssfct  12256  isprm2  12258  phicl2  12355  hashdvds  12362  phisum  12381  odzval  12382  odzcllem  12383  odzdvds  12386  oddennn  12552  evenennn  12553  znnen  12558  ennnfonelemg  12563  ennnfonelemom  12568  ismhm  13036  issubm  13047  issubmd  13049  grplinv  13125  issubg  13246  isnsg  13275  isrim0  13660  issubrng  13698  issubrg  13720  islssm  13856  islssmg  13857  cnfldui  14088  istopon  14192  epttop  14269  iscld  14282  isnei  14323  neipsm  14333  iscn  14376  iscnp  14378  txdis1cn  14457  ishmeo  14483  ispsmet  14502  ismet  14523  isxmet  14524  elblps  14569  elbl  14570  xmetxpbl  14687  reopnap  14725  divcnap  14744  elcncf  14752  cdivcncfap  14783  cnopnap  14790  divcncfap  14793  maxcncf  14794  mincncf  14795  ellimc3apf  14839  limccoap  14857  dvlemap  14859  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvcnp2cntop  14878  dvaddxxbr  14880  dvmulxxbr  14881  dvcoapbr  14886  dvcjbr  14887  dvrecap  14892  dveflem  14905  lgsfle1  15166  lgsle1  15172  lgsdirprm  15191  lgsne0  15195  lgsquadlem1  15234  lgsquadlem2  15235  subctctexmid  15561