Theorem elrab 2936

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

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

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rab 2495  df-v 2778

This theorem is referenced by:  elrab3  2937  elrabd  2938  elrab2  2939  ralrab  2941  rexrab  2943  rabsnt  3718  unimax  3898  ssintub  3917  intminss  3924  exmidexmid  4256  exmidsssnc  4263  rabxfrd  4534  ordtri2or2exmidlem  4592  onsucelsucexmidlem1  4594  sefvex  5620  ssimaex  5663  acexmidlem2  5964  elpmg  6774  ssfilem  6998  diffitest  7010  inffiexmid  7029  supubti  7127  suplubti  7128  ctssexmid  7278  exmidonfinlem  7332  finacn  7347  cc4f  7416  cc4n  7418  acnccim  7419  caucvgprlemladdfu  7825  caucvgprlemladdrl  7826  suplocexprlemmu  7866  suplocexprlemru  7867  suplocexprlemdisj  7868  suplocexprlemub  7871  nnindnn  8041  negf1o  8489  apsscn  8755  sup3exmid  9065  nnind  9087  peano2uz2  9515  peano5uzti  9516  dfuzi  9518  uzind  9519  uzind3  9521  eluz1  9687  uzind4  9744  supinfneg  9751  infsupneg  9752  eqreznegel  9770  elixx1  10054  elioo2  10078  elfz1  10170  zsupcl  10411  infssuzex  10413  infssuzcldc  10415  expcl2lemap  10733  expclzaplem  10745  expclzap  10746  expap0i  10753  expge0  10757  expge1  10758  hashennnuni  10961  wrdmap  11062  shftf  11256  reccn2ap  11739  dvdsdivcl  12276  divalgmod  12353  bitsval  12369  bitsfzolem  12380  bezoutlemsup  12445  dfgcd2  12450  uzwodc  12473  nnwosdc  12475  nninfctlemfo  12476  lcmgcdlem  12514  1nprm  12551  1idssfct  12552  isprm2  12554  phicl2  12651  hashdvds  12658  dvdsfi  12676  phisum  12678  odzval  12679  odzcllem  12680  odzdvds  12683  oddennn  12878  evenennn  12879  znnen  12884  ennnfonelemg  12889  ennnfonelemom  12894  ismhm  13408  issubm  13419  issubmd  13421  grplinv  13497  issubg  13624  isnsg  13653  isrim0  14038  issubrng  14076  issubrg  14098  islssm  14234  islssmg  14235  cnfldui  14466  mplelbascoe  14569  istopon  14600  epttop  14677  iscld  14690  isnei  14731  neipsm  14741  iscn  14784  iscnp  14786  txdis1cn  14865  ishmeo  14891  ispsmet  14910  ismet  14931  isxmet  14932  elblps  14977  elbl  14978  xmetxpbl  15095  reopnap  15133  divcnap  15152  elcncf  15160  cdivcncfap  15191  cnopnap  15198  divcncfap  15201  maxcncf  15202  mincncf  15203  ellimc3apf  15247  limccoap  15265  dvlemap  15267  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dvcnp2cntop  15286  dvaddxxbr  15288  dvmulxxbr  15289  dvcoapbr  15294  dvcjbr  15295  dvrecap  15300  dveflem  15313  dvdsppwf1o  15576  lgsfle1  15601  lgsle1  15607  lgsdirprm  15626  lgsne0  15630  lgsquadlem1  15669  lgsquadlem2  15670  uhgrm  15789  upgrm  15811  upgr1or2  15812  umgredg2en  15820  umgrbien  15821  uhgredgm  15842  edgupgren  15845  edgumgren  15846  2omap  16132  pw1map  16134  subctctexmid  16139