Theorem elrab2 2939

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 2274	. 2 |- ( A e. C <-> A e. { x e. B | ph } )
3		elrab2.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elrab 2936	. 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 1373   e. wcel 2178   {crab 2490

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rab 2495  df-v 2778

This theorem is referenced by:  elrabsf  3044  pwnss  4219  regexmidlemm  4598  regexmidlem1  4599  reg2exmidlema  4600  tfis  4649  ctssdccl  7239  nninff  7250  nninfninc  7251  infnninf  7252  infnninfOLD  7253  nnnninf  7254  nnnninfeq  7256  nnnninfeq2  7257  nninfwlpoimlemg  7303  exmidaclem  7351  ltexprlemell  7746  ltexprlemelu  7747  cauappcvgprlemm  7793  cauappcvgprlemopl  7794  cauappcvgprlemlol  7795  cauappcvgprlemopu  7796  cauappcvgprlemupu  7797  cauappcvgprlemdisj  7799  cauappcvgprlemloc  7800  cauappcvgprlemladdfu  7802  cauappcvgprlemladdfl  7803  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlem2  7808  caucvgprlemm  7816  caucvgprlemopl  7817  caucvgprlemlol  7818  caucvgprlemopu  7819  caucvgprlemupu  7820  caucvgprlemdisj  7822  caucvgprlemloc  7823  caucvgprlemladdfu  7825  caucvgprlem2  7828  caucvgprprlemell  7833  caucvgprprlemelu  7834  caucvgprprlemml  7842  caucvgprprlemmu  7843  caucvgprprlemexbt  7854  caucvgprprlem2  7858  suplocsrlemb  7954  suplocsrlempr  7955  suplocsrlem  7956  axpre-suploclemres  8049  elz  9409  elrp  9812  repos  10127  zsupssdc  10418  bitsfzolem  12380  isprm  12546  oddpwdc  12611  sqpweven  12612  2sqpwodd  12613  phimullem  12662  eulerthlem1  12664  eulerthlemfi  12665  eulerthlemrprm  12666  eulerthlemth  12669  hashgcdlem  12675  pclem0  12724  pclemub  12725  pclemdc  12726  pcprecl  12727  pcprendvds  12728  1arith  12805  elgz  12809  4sqlem13m  12841  4sqlem17  12845  4sqlem18  12846  ctiunctlemu1st  12920  ctiunctlemu2nd  12921  ctiunctlemudc  12923  ctiunctlemfo  12925  infpn2  12942  issgrp  13350  ismnddef  13365  gsumvallem2  13440  isgrp  13453  elnmz  13659  iscmn  13744  isrng  13811  issrg  13842  isring  13877  iscrng  13880  isnzr  14058  islring  14069  isrrg  14140  isdomn  14146  islmod  14168  psrbag  14546  psr1clfi  14565  isxms  15038  isms  15040  ivthinclemlm  15221  ivthinclemum  15222  ivthinclemlopn  15223  ivthinclemlr  15224  ivthinclemuopn  15225  ivthinclemur  15226  ivthinclemdisj  15227  ivthinclemloc  15228  mpodvdsmulf1o  15577  lgslem2  15593  lgslem3  15594  lgsfcl2  15598  lfgredg2dom  15838  0nninf  16143  nnsf  16144  peano4nninf  16145  nninfalllem1  16147  nninfself  16152  qdencn  16168