Theorem elrab 2893

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1353   e. wcel 2148   {crab 2459

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-v 2739

This theorem is referenced by:  elrab3  2894  elrabd  2895  elrab2  2896  ralrab  2898  rexrab  2900  rabsnt  3667  unimax  3843  ssintub  3862  intminss  3869  exmidexmid  4195  exmidsssnc  4202  rabxfrd  4468  ordtri2or2exmidlem  4524  onsucelsucexmidlem1  4526  sefvex  5535  ssimaex  5576  acexmidlem2  5869  elpmg  6661  ssfilem  6872  diffitest  6884  inffiexmid  6903  supubti  6995  suplubti  6996  ctssexmid  7145  exmidonfinlem  7189  cc4f  7265  cc4n  7267  caucvgprlemladdfu  7673  caucvgprlemladdrl  7674  suplocexprlemmu  7714  suplocexprlemru  7715  suplocexprlemdisj  7716  suplocexprlemub  7719  nnindnn  7889  negf1o  8335  apsscn  8600  sup3exmid  8910  nnind  8931  peano2uz2  9356  peano5uzti  9357  dfuzi  9359  uzind  9360  uzind3  9362  eluz1  9528  uzind4  9584  supinfneg  9591  infsupneg  9592  eqreznegel  9610  elixx1  9893  elioo2  9917  elfz1  10009  expcl2lemap  10527  expclzaplem  10539  expclzap  10540  expap0i  10547  expge0  10551  expge1  10552  hashennnuni  10752  shftf  10832  reccn2ap  11314  dvdsdivcl  11848  divalgmod  11924  zsupcl  11940  infssuzex  11942  infssuzcldc  11944  bezoutlemsup  12002  dfgcd2  12007  uzwodc  12030  nnwosdc  12032  lcmcllem  12059  lcmledvds  12062  lcmgcdlem  12069  1nprm  12106  1idssfct  12107  isprm2  12109  phicl2  12206  hashdvds  12213  phisum  12232  odzval  12233  odzcllem  12234  odzdvds  12237  oddennn  12385  evenennn  12386  znnen  12391  ennnfonelemg  12396  ennnfonelemom  12401  ismhm  12785  issubm  12795  issubmd  12797  grplinv  12854  issubg  12964  isnsg  12993  issubrg  13280  istopon  13382  epttop  13461  iscld  13474  isnei  13515  neipsm  13525  iscn  13568  iscnp  13570  txdis1cn  13649  ishmeo  13675  ispsmet  13694  ismet  13715  isxmet  13716  elblps  13761  elbl  13762  xmetxpbl  13879  reopnap  13909  divcnap  13926  elcncf  13931  cdivcncfap  13958  cnopnap  13965  ellimc3apf  14000  limccoap  14018  dvlemap  14020  dvidlemap  14031  dvcnp2cntop  14034  dvaddxxbr  14036  dvmulxxbr  14037  dvcoapbr  14042  dvcjbr  14043  dvrecap  14048  dveflem  14058  lgsfle1  14281  lgsle1  14287  lgsdirprm  14306  lgsne0  14310  subctctexmid  14610