Theorem elrab2 2966

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 2963	. 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 2202   {crab 2515

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rab 2520  df-v 2805

This theorem is referenced by:  elrabsf  3071  pwnss  4255  regexmidlemm  4636  regexmidlem1  4637  reg2exmidlema  4638  tfis  4687  ctssdccl  7370  nninff  7381  nninfninc  7382  infnninf  7383  infnninfOLD  7384  nnnninf  7385  nnnninfeq  7387  nnnninfeq2  7388  nninfwlpoimlemg  7434  exmidaclem  7483  ltexprlemell  7878  ltexprlemelu  7879  cauappcvgprlemm  7925  cauappcvgprlemopl  7926  cauappcvgprlemlol  7927  cauappcvgprlemopu  7928  cauappcvgprlemupu  7929  cauappcvgprlemdisj  7931  cauappcvgprlemloc  7932  cauappcvgprlemladdfu  7934  cauappcvgprlemladdfl  7935  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  cauappcvgprlem2  7940  caucvgprlemm  7948  caucvgprlemopl  7949  caucvgprlemlol  7950  caucvgprlemopu  7951  caucvgprlemupu  7952  caucvgprlemdisj  7954  caucvgprlemloc  7955  caucvgprlemladdfu  7957  caucvgprlem2  7960  caucvgprprlemell  7965  caucvgprprlemelu  7966  caucvgprprlemml  7974  caucvgprprlemmu  7975  caucvgprprlemexbt  7986  caucvgprprlem2  7990  suplocsrlemb  8086  suplocsrlempr  8087  suplocsrlem  8088  axpre-suploclemres  8181  elz  9542  elrp  9951  repos  10266  zsupssdc  10561  bitsfzolem  12595  isprm  12761  oddpwdc  12826  sqpweven  12827  2sqpwodd  12828  phimullem  12877  eulerthlem1  12879  eulerthlemfi  12880  eulerthlemrprm  12881  eulerthlemth  12884  hashgcdlem  12890  pclem0  12939  pclemub  12940  pclemdc  12941  pcprecl  12942  pcprendvds  12943  1arith  13020  elgz  13024  4sqlem13m  13056  4sqlem17  13060  4sqlem18  13061  ctiunctlemu1st  13135  ctiunctlemu2nd  13136  ctiunctlemudc  13138  ctiunctlemfo  13140  infpn2  13157  issgrp  13566  ismnddef  13581  gsumvallem2  13656  isgrp  13669  elnmz  13875  iscmn  13960  isrng  14028  issrg  14059  isring  14094  iscrng  14097  isnzr  14276  islring  14287  isrrg  14358  isdomn  14365  islmod  14387  psrbag  14765  psrbagconcl  14773  psr1clfi  14789  isxms  15262  isms  15264  ivthinclemlm  15445  ivthinclemum  15446  ivthinclemlopn  15447  ivthinclemlr  15448  ivthinclemuopn  15449  ivthinclemur  15450  ivthinclemdisj  15451  ivthinclemloc  15452  mpodvdsmulf1o  15804  lgslem2  15820  lgslem3  15821  lgsfcl2  15825  lfgredg2dom  16073  uspgredg2vlem  16161  uspgredg2v  16162  usgredg2vlem1  16163  usgredg2vlem2  16164  ushgredgedg  16167  ushgredgedgloop  16169  isclwwlknon  16371  s2elclwwlknon2  16377  0nninf  16730  nnsf  16731  peano4nninf  16732  nninfalllem1  16734  nninfself  16739  qdencn  16755