Theorem elrab2 2979

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 2301	. 2 |- ( A e. C <-> A e. { x e. B | ph } )
3		elrab2.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elrab 2976	. 2 |- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )
5	2, 4	bitri 184	1 |- ( A e. C <-> ( A e. B /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1398   e. wcel 2205   {crab 2526

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rab 2531  df-v 2817

This theorem is referenced by:  elrabsf  3084  pwnss  4278  regexmidlemm  4661  regexmidlem1  4662  reg2exmidlema  4663  tfis  4712  ctssdccl  7417  nninff  7428  nninfninc  7429  infnninf  7430  infnninfOLD  7431  nnnninf  7432  nnnninfeq  7434  nnnninfeq2  7435  nninfwlpoimlemg  7481  exmidaclem  7530  ltexprlemell  7931  ltexprlemelu  7932  cauappcvgprlemm  7978  cauappcvgprlemopl  7979  cauappcvgprlemlol  7980  cauappcvgprlemopu  7981  cauappcvgprlemupu  7982  cauappcvgprlemdisj  7984  cauappcvgprlemloc  7985  cauappcvgprlemladdfu  7987  cauappcvgprlemladdfl  7988  cauappcvgprlemladdru  7989  cauappcvgprlemladdrl  7990  cauappcvgprlem2  7993  caucvgprlemm  8001  caucvgprlemopl  8002  caucvgprlemlol  8003  caucvgprlemopu  8004  caucvgprlemupu  8005  caucvgprlemdisj  8007  caucvgprlemloc  8008  caucvgprlemladdfu  8010  caucvgprlem2  8013  caucvgprprlemell  8018  caucvgprprlemelu  8019  caucvgprprlemml  8027  caucvgprprlemmu  8028  caucvgprprlemexbt  8039  caucvgprprlem2  8043  suplocsrlemb  8139  suplocsrlempr  8140  suplocsrlem  8141  axpre-suploclemres  8234  elz  9601  elrp  10011  repos  10327  zsupssdc  10627  bitsfzolem  12671  isprm  12837  oddpwdc  12902  sqpweven  12903  2sqpwodd  12904  phimullem  12953  eulerthlem1  12955  eulerthlemfi  12956  eulerthlemrprm  12957  eulerthlemth  12960  hashgcdlem  12966  pclem0  13015  pclemub  13016  pclemdc  13017  pcprecl  13018  pcprendvds  13019  1arith  13096  elgz  13100  4sqlem13m  13132  4sqlem17  13136  4sqlem18  13137  ballotfilemelo  13172  ballotfileme  13186  ballotfilemscl  13197  ctiunctlemu1st  13275  ctiunctlemu2nd  13276  ctiunctlemudc  13278  ctiunctlemfo  13280  infpn2  13297  issgrp  13672  ismnddef  13685  gsumvallem2  13754  isgrp  13767  elnmz  13967  iscmn  14052  isrng  14179  issrg  14214  isring  14249  iscrng  14252  isnzr  14432  islring  14443  isrrg  14515  isdomn  14522  isdrngtap  14550  islmod  14571  psrbag  14949  psrbagconcl  14959  psr1clfi  14975  isxms  15448  isms  15450  ivthinclemlm  15631  ivthinclemum  15632  ivthinclemlopn  15633  ivthinclemlr  15634  ivthinclemuopn  15635  ivthinclemur  15636  ivthinclemdisj  15637  ivthinclemloc  15638  mpodvdsmulf1o  15990  lgslem2  16006  lgslem3  16007  lgsfcl2  16011  lfgredg2dom  16259  uspgredg2vlem  16347  uspgredg2v  16348  usgredg2vlem1  16349  usgredg2vlem2  16350  ushgredgedg  16353  ushgredgedgloop  16355  isclwwlknon  16557  s2elclwwlknon2  16563  0nninf  16924  nnsf  16925  peano4nninf  16926  nninfalllem1  16928  nninfself  16933  qdencn  16949