Theorem elrab2 2932

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 2272	. 2 |- ( A e. C <-> A e. { x e. B | ph } )
3		elrab2.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elrab 2929	. 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 2176   {crab 2488

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rab 2493  df-v 2774

This theorem is referenced by:  elrabsf  3037  pwnss  4204  regexmidlemm  4581  regexmidlem1  4582  reg2exmidlema  4583  tfis  4632  ctssdccl  7215  nninff  7226  nninfninc  7227  infnninf  7228  infnninfOLD  7229  nnnninf  7230  nnnninfeq  7232  nnnninfeq2  7233  nninfwlpoimlemg  7279  exmidaclem  7322  ltexprlemell  7713  ltexprlemelu  7714  cauappcvgprlemm  7760  cauappcvgprlemopl  7761  cauappcvgprlemlol  7762  cauappcvgprlemopu  7763  cauappcvgprlemupu  7764  cauappcvgprlemdisj  7766  cauappcvgprlemloc  7767  cauappcvgprlemladdfu  7769  cauappcvgprlemladdfl  7770  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  cauappcvgprlem2  7775  caucvgprlemm  7783  caucvgprlemopl  7784  caucvgprlemlol  7785  caucvgprlemopu  7786  caucvgprlemupu  7787  caucvgprlemdisj  7789  caucvgprlemloc  7790  caucvgprlemladdfu  7792  caucvgprlem2  7795  caucvgprprlemell  7800  caucvgprprlemelu  7801  caucvgprprlemml  7809  caucvgprprlemmu  7810  caucvgprprlemexbt  7821  caucvgprprlem2  7825  suplocsrlemb  7921  suplocsrlempr  7922  suplocsrlem  7923  axpre-suploclemres  8016  elz  9376  elrp  9779  repos  10094  zsupssdc  10383  bitsfzolem  12298  isprm  12464  oddpwdc  12529  sqpweven  12530  2sqpwodd  12531  phimullem  12580  eulerthlem1  12582  eulerthlemfi  12583  eulerthlemrprm  12584  eulerthlemth  12587  hashgcdlem  12593  pclem0  12642  pclemub  12643  pclemdc  12644  pcprecl  12645  pcprendvds  12646  1arith  12723  elgz  12727  4sqlem13m  12759  4sqlem17  12763  4sqlem18  12764  ctiunctlemu1st  12838  ctiunctlemu2nd  12839  ctiunctlemudc  12841  ctiunctlemfo  12843  infpn2  12860  issgrp  13268  ismnddef  13283  gsumvallem2  13358  isgrp  13371  elnmz  13577  iscmn  13662  isrng  13729  issrg  13760  isring  13795  iscrng  13798  isnzr  13976  islring  13987  isrrg  14058  isdomn  14064  islmod  14086  psrbag  14464  psr1clfi  14483  isxms  14956  isms  14958  ivthinclemlm  15139  ivthinclemum  15140  ivthinclemlopn  15141  ivthinclemlr  15142  ivthinclemuopn  15143  ivthinclemur  15144  ivthinclemdisj  15145  ivthinclemloc  15146  mpodvdsmulf1o  15495  lgslem2  15511  lgslem3  15512  lgsfcl2  15516  0nninf  15978  nnsf  15979  peano4nninf  15980  nninfalllem1  15982  nninfself  15987  qdencn  16003