Theorem elrab2 2871

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 2224	. 2 |- ( A e. C <-> A e. { x e. B | ph } )
3		elrab2.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elrab 2868	. 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 1335   e. wcel 2128   {crab 2439

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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rab 2444  df-v 2714

This theorem is referenced by:  elrabsf  2975  pwnss  4120  regexmidlemm  4490  regexmidlem1  4491  reg2exmidlema  4492  tfis  4541  ctssdccl  7049  nninff  7060  infnninf  7061  infnninfOLD  7062  nnnninf  7063  nnnninfeq  7065  nnnninfeq2  7066  exmidaclem  7137  ltexprlemell  7512  ltexprlemelu  7513  cauappcvgprlemm  7559  cauappcvgprlemopl  7560  cauappcvgprlemlol  7561  cauappcvgprlemopu  7562  cauappcvgprlemupu  7563  cauappcvgprlemdisj  7565  cauappcvgprlemloc  7566  cauappcvgprlemladdfu  7568  cauappcvgprlemladdfl  7569  cauappcvgprlemladdru  7570  cauappcvgprlemladdrl  7571  cauappcvgprlem2  7574  caucvgprlemm  7582  caucvgprlemopl  7583  caucvgprlemlol  7584  caucvgprlemopu  7585  caucvgprlemupu  7586  caucvgprlemdisj  7588  caucvgprlemloc  7589  caucvgprlemladdfu  7591  caucvgprlem2  7594  caucvgprprlemell  7599  caucvgprprlemelu  7600  caucvgprprlemml  7608  caucvgprprlemmu  7609  caucvgprprlemexbt  7620  caucvgprprlem2  7624  suplocsrlemb  7720  suplocsrlempr  7721  suplocsrlem  7722  axpre-suploclemres  7815  elz  9163  elrp  9555  repos  9867  isprm  11977  oddpwdc  12039  sqpweven  12040  2sqpwodd  12041  phimullem  12088  eulerthlem1  12090  eulerthlemfi  12091  eulerthlemrprm  12092  eulerthlemth  12095  hashgcdlem  12101  ctiunctlemu1st  12146  ctiunctlemu2nd  12147  ctiunctlemudc  12149  ctiunctlemfo  12151  isxms  12822  isms  12824  ivthinclemlm  12983  ivthinclemum  12984  ivthinclemlopn  12985  ivthinclemlr  12986  ivthinclemuopn  12987  ivthinclemur  12988  ivthinclemdisj  12989  ivthinclemloc  12990  0nninf  13547  nnsf  13548  peano4nninf  13549  nninfalllem1  13551  nninfself  13556  qdencn  13569