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  4203  regexmidlemm  4580  regexmidlem1  4581  reg2exmidlema  4582  tfis  4631  ctssdccl  7213  nninff  7224  nninfninc  7225  infnninf  7226  infnninfOLD  7227  nnnninf  7228  nnnninfeq  7230  nnnninfeq2  7231  nninfwlpoimlemg  7277  exmidaclem  7320  ltexprlemell  7711  ltexprlemelu  7712  cauappcvgprlemm  7758  cauappcvgprlemopl  7759  cauappcvgprlemlol  7760  cauappcvgprlemopu  7761  cauappcvgprlemupu  7762  cauappcvgprlemdisj  7764  cauappcvgprlemloc  7765  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  cauappcvgprlem2  7773  caucvgprlemm  7781  caucvgprlemopl  7782  caucvgprlemlol  7783  caucvgprlemopu  7784  caucvgprlemupu  7785  caucvgprlemdisj  7787  caucvgprlemloc  7788  caucvgprlemladdfu  7790  caucvgprlem2  7793  caucvgprprlemell  7798  caucvgprprlemelu  7799  caucvgprprlemml  7807  caucvgprprlemmu  7808  caucvgprprlemexbt  7819  caucvgprprlem2  7823  suplocsrlemb  7919  suplocsrlempr  7920  suplocsrlem  7921  axpre-suploclemres  8014  elz  9374  elrp  9777  repos  10092  zsupssdc  10381  bitsfzolem  12265  isprm  12431  oddpwdc  12496  sqpweven  12497  2sqpwodd  12498  phimullem  12547  eulerthlem1  12549  eulerthlemfi  12550  eulerthlemrprm  12551  eulerthlemth  12554  hashgcdlem  12560  pclem0  12609  pclemub  12610  pclemdc  12611  pcprecl  12612  pcprendvds  12613  1arith  12690  elgz  12694  4sqlem13m  12726  4sqlem17  12730  4sqlem18  12731  ctiunctlemu1st  12805  ctiunctlemu2nd  12806  ctiunctlemudc  12808  ctiunctlemfo  12810  infpn2  12827  issgrp  13235  ismnddef  13250  gsumvallem2  13325  isgrp  13338  elnmz  13544  iscmn  13629  isrng  13696  issrg  13727  isring  13762  iscrng  13765  isnzr  13943  islring  13954  isrrg  14025  isdomn  14031  islmod  14053  psrbag  14431  psr1clfi  14450  isxms  14923  isms  14925  ivthinclemlm  15106  ivthinclemum  15107  ivthinclemlopn  15108  ivthinclemlr  15109  ivthinclemuopn  15110  ivthinclemur  15111  ivthinclemdisj  15112  ivthinclemloc  15113  mpodvdsmulf1o  15462  lgslem2  15478  lgslem3  15479  lgsfcl2  15483  0nninf  15945  nnsf  15946  peano4nninf  15947  nninfalllem1  15949  nninfself  15954  qdencn  15970