Theorem elrab2 2965

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 2298	. 2 |- ( A e. C <-> A e. { x e. B | ph } )
3		elrab2.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elrab 2962	. 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 1397   e. wcel 2202   {crab 2514

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rab 2519  df-v 2804

This theorem is referenced by:  elrabsf  3070  pwnss  4249  regexmidlemm  4630  regexmidlem1  4631  reg2exmidlema  4632  tfis  4681  ctssdccl  7310  nninff  7321  nninfninc  7322  infnninf  7323  infnninfOLD  7324  nnnninf  7325  nnnninfeq  7327  nnnninfeq2  7328  nninfwlpoimlemg  7374  exmidaclem  7423  ltexprlemell  7818  ltexprlemelu  7819  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem2  7880  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemladdfu  7897  caucvgprlem2  7900  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemexbt  7926  caucvgprprlem2  7930  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  axpre-suploclemres  8121  elz  9481  elrp  9890  repos  10205  zsupssdc  10499  bitsfzolem  12533  isprm  12699  oddpwdc  12764  sqpweven  12765  2sqpwodd  12766  phimullem  12815  eulerthlem1  12817  eulerthlemfi  12818  eulerthlemrprm  12819  eulerthlemth  12822  hashgcdlem  12828  pclem0  12877  pclemub  12878  pclemdc  12879  pcprecl  12880  pcprendvds  12881  1arith  12958  elgz  12962  4sqlem13m  12994  4sqlem17  12998  4sqlem18  12999  ctiunctlemu1st  13073  ctiunctlemu2nd  13074  ctiunctlemudc  13076  ctiunctlemfo  13078  infpn2  13095  issgrp  13504  ismnddef  13519  gsumvallem2  13594  isgrp  13607  elnmz  13813  iscmn  13898  isrng  13966  issrg  13997  isring  14032  iscrng  14035  isnzr  14214  islring  14225  isrrg  14296  isdomn  14302  islmod  14324  psrbag  14702  psr1clfi  14721  isxms  15194  isms  15196  ivthinclemlm  15377  ivthinclemum  15378  ivthinclemlopn  15379  ivthinclemlr  15380  ivthinclemuopn  15381  ivthinclemur  15382  ivthinclemdisj  15383  ivthinclemloc  15384  mpodvdsmulf1o  15733  lgslem2  15749  lgslem3  15750  lgsfcl2  15754  lfgredg2dom  16002  uspgredg2vlem  16090  uspgredg2v  16091  usgredg2vlem1  16092  usgredg2vlem2  16093  ushgredgedg  16096  ushgredgedgloop  16098  isclwwlknon  16300  s2elclwwlknon2  16306  0nninf  16657  nnsf  16658  peano4nninf  16659  nninfalllem1  16661  nninfself  16666  qdencn  16682