Theorem elrab2 2847

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 2207	. 2 |- ( A e. C <-> A e. { x e. B | ph } )
3		elrab2.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elrab 2844	. 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 1332   e. wcel 1481   {crab 2421

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rab 2426  df-v 2691

This theorem is referenced by:  elrabsf  2951  pwnss  4091  regexmidlemm  4455  regexmidlem1  4456  reg2exmidlema  4457  tfis  4505  ctssdccl  7004  infnninf  7030  nnnninf  7031  exmidaclem  7081  ltexprlemell  7430  ltexprlemelu  7431  cauappcvgprlemm  7477  cauappcvgprlemopl  7478  cauappcvgprlemlol  7479  cauappcvgprlemopu  7480  cauappcvgprlemupu  7481  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgprlem2  7492  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemlol  7502  caucvgprlemopu  7503  caucvgprlemupu  7504  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlemladdfu  7509  caucvgprlem2  7512  caucvgprprlemell  7517  caucvgprprlemelu  7518  caucvgprprlemml  7526  caucvgprprlemmu  7527  caucvgprprlemexbt  7538  caucvgprprlem2  7542  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  axpre-suploclemres  7733  elz  9080  elrp  9472  repos  9783  isprm  11826  oddpwdc  11888  sqpweven  11889  2sqpwodd  11890  phimullem  11937  hashgcdlem  11939  ctiunctlemu1st  11983  ctiunctlemu2nd  11984  ctiunctlemudc  11986  ctiunctlemfo  11988  isxms  12659  isms  12661  ivthinclemlm  12820  ivthinclemum  12821  ivthinclemlopn  12822  ivthinclemlr  12823  ivthinclemuopn  12824  ivthinclemur  12825  ivthinclemdisj  12826  ivthinclemloc  12827  0nninf  13372  nninff  13373  nnsf  13374  peano4nninf  13375  nninfalllemn  13377  nninfalllem1  13378  nninfself  13384  qdencn  13397