Theorem elrab2 2898

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 2244	. 2 |- ( A e. C <-> A e. { x e. B | ph } )
3		elrab2.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elrab 2895	. 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 1353   e. wcel 2148   {crab 2459

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-v 2741

This theorem is referenced by:  elrabsf  3003  pwnss  4161  regexmidlemm  4533  regexmidlem1  4534  reg2exmidlema  4535  tfis  4584  ctssdccl  7112  nninff  7123  infnninf  7124  infnninfOLD  7125  nnnninf  7126  nnnninfeq  7128  nnnninfeq2  7129  nninfwlpoimlemg  7175  exmidaclem  7209  ltexprlemell  7599  ltexprlemelu  7600  cauappcvgprlemm  7646  cauappcvgprlemopl  7647  cauappcvgprlemlol  7648  cauappcvgprlemopu  7649  cauappcvgprlemupu  7650  cauappcvgprlemdisj  7652  cauappcvgprlemloc  7653  cauappcvgprlemladdfu  7655  cauappcvgprlemladdfl  7656  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  cauappcvgprlem2  7661  caucvgprlemm  7669  caucvgprlemopl  7670  caucvgprlemlol  7671  caucvgprlemopu  7672  caucvgprlemupu  7673  caucvgprlemdisj  7675  caucvgprlemloc  7676  caucvgprlemladdfu  7678  caucvgprlem2  7681  caucvgprprlemell  7686  caucvgprprlemelu  7687  caucvgprprlemml  7695  caucvgprprlemmu  7696  caucvgprprlemexbt  7707  caucvgprprlem2  7711  suplocsrlemb  7807  suplocsrlempr  7808  suplocsrlem  7809  axpre-suploclemres  7902  elz  9257  elrp  9657  repos  9972  zsupssdc  11957  isprm  12111  oddpwdc  12176  sqpweven  12177  2sqpwodd  12178  phimullem  12227  eulerthlem1  12229  eulerthlemfi  12230  eulerthlemrprm  12231  eulerthlemth  12234  hashgcdlem  12240  pclem0  12288  pclemub  12289  pclemdc  12290  pcprecl  12291  pcprendvds  12292  1arith  12367  elgz  12371  ctiunctlemu1st  12437  ctiunctlemu2nd  12438  ctiunctlemudc  12440  ctiunctlemfo  12442  infpn2  12459  issgrp  12814  ismnddef  12824  isgrp  12888  elnmz  13073  iscmn  13101  issrg  13153  isring  13188  iscrng  13191  isnzr  13330  islring  13338  islmod  13386  isxms  13990  isms  13992  ivthinclemlm  14151  ivthinclemum  14152  ivthinclemlopn  14153  ivthinclemlr  14154  ivthinclemuopn  14155  ivthinclemur  14156  ivthinclemdisj  14157  ivthinclemloc  14158  lgslem2  14441  lgslem3  14442  lgsfcl2  14446  0nninf  14792  nnsf  14793  peano4nninf  14794  nninfalllem1  14796  nninfself  14801  qdencn  14814