Theorem elrab2 2884

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.)

Hypotheses

Ref	Expression
elrab2.1	|- ( x = A -> ( ph <-> ps ) )
elrab2.2	|- C = { x e. B | ph }

Assertion

Ref	Expression
elrab2	|- ( A e. C <-> ( A e. B /\ ps ) )

Distinct variable groups:   ps, x   x, A   x, B

Allowed substitution hints:   ph( x)   C( x)

Proof of Theorem elrab2

Step	Hyp	Ref	Expression
1		elrab2.2	. . 3 |- C = { x e. B | ph }
2	1	eleq2i 2232	. 2 |- ( A e. C <-> A e. { x e. B | ph } )
3		elrab2.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elrab 2881	. 2 |- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )
5	2, 4	bitri 183	1 |- ( A e. C <-> ( A e. B /\ ps ) )

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

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 2296  df-rab 2452  df-v 2727

This theorem is referenced by:  elrabsf  2988  pwnss  4137  regexmidlemm  4508  regexmidlem1  4509  reg2exmidlema  4510  tfis  4559  ctssdccl  7072  nninff  7083  infnninf  7084  infnninfOLD  7085  nnnninf  7086  nnnninfeq  7088  nnnninfeq2  7089  exmidaclem  7160  ltexprlemell  7535  ltexprlemelu  7536  cauappcvgprlemm  7582  cauappcvgprlemopl  7583  cauappcvgprlemlol  7584  cauappcvgprlemopu  7585  cauappcvgprlemupu  7586  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlemladdfu  7591  cauappcvgprlemladdfl  7592  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgprlem2  7597  caucvgprlemm  7605  caucvgprlemopl  7606  caucvgprlemlol  7607  caucvgprlemopu  7608  caucvgprlemupu  7609  caucvgprlemdisj  7611  caucvgprlemloc  7612  caucvgprlemladdfu  7614  caucvgprlem2  7617  caucvgprprlemell  7622  caucvgprprlemelu  7623  caucvgprprlemml  7631  caucvgprprlemmu  7632  caucvgprprlemexbt  7643  caucvgprprlem2  7647  suplocsrlemb  7743  suplocsrlempr  7744  suplocsrlem  7745  axpre-suploclemres  7838  elz  9189  elrp  9587  repos  9902  zsupssdc  11883  isprm  12037  oddpwdc  12102  sqpweven  12103  2sqpwodd  12104  phimullem  12153  eulerthlem1  12155  eulerthlemfi  12156  eulerthlemrprm  12157  eulerthlemth  12160  hashgcdlem  12166  pclem0  12214  pclemub  12215  pclemdc  12216  pcprecl  12217  pcprendvds  12218  1arith  12293  elgz  12297  ctiunctlemu1st  12363  ctiunctlemu2nd  12364  ctiunctlemudc  12366  ctiunctlemfo  12368  infpn2  12385  isxms  13051  isms  13053  ivthinclemlm  13212  ivthinclemum  13213  ivthinclemlopn  13214  ivthinclemlr  13215  ivthinclemuopn  13216  ivthinclemur  13217  ivthinclemdisj  13218  ivthinclemloc  13219  lgslem2  13502  lgslem3  13503  lgsfcl2  13507  0nninf  13844  nnsf  13845  peano4nninf  13846  nninfalllem1  13848  nninfself  13853  qdencn  13866