Theorem elrab2 2923

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 2263	. 2 |- ( A e. C <-> A e. { x e. B | ph } )
3		elrab2.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elrab 2920	. 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 1364   e. wcel 2167   {crab 2479

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rab 2484  df-v 2765

This theorem is referenced by:  elrabsf  3028  pwnss  4193  regexmidlemm  4569  regexmidlem1  4570  reg2exmidlema  4571  tfis  4620  ctssdccl  7186  nninff  7197  nninfninc  7198  infnninf  7199  infnninfOLD  7200  nnnninf  7201  nnnninfeq  7203  nnnninfeq2  7204  nninfwlpoimlemg  7250  exmidaclem  7291  ltexprlemell  7682  ltexprlemelu  7683  cauappcvgprlemm  7729  cauappcvgprlemopl  7730  cauappcvgprlemlol  7731  cauappcvgprlemopu  7732  cauappcvgprlemupu  7733  cauappcvgprlemdisj  7735  cauappcvgprlemloc  7736  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlem2  7744  caucvgprlemm  7752  caucvgprlemopl  7753  caucvgprlemlol  7754  caucvgprlemopu  7755  caucvgprlemupu  7756  caucvgprlemdisj  7758  caucvgprlemloc  7759  caucvgprlemladdfu  7761  caucvgprlem2  7764  caucvgprprlemell  7769  caucvgprprlemelu  7770  caucvgprprlemml  7778  caucvgprprlemmu  7779  caucvgprprlemexbt  7790  caucvgprprlem2  7794  suplocsrlemb  7890  suplocsrlempr  7891  suplocsrlem  7892  axpre-suploclemres  7985  elz  9345  elrp  9747  repos  10062  zsupssdc  10345  bitsfzolem  12136  isprm  12302  oddpwdc  12367  sqpweven  12368  2sqpwodd  12369  phimullem  12418  eulerthlem1  12420  eulerthlemfi  12421  eulerthlemrprm  12422  eulerthlemth  12425  hashgcdlem  12431  pclem0  12480  pclemub  12481  pclemdc  12482  pcprecl  12483  pcprendvds  12484  1arith  12561  elgz  12565  4sqlem13m  12597  4sqlem17  12601  4sqlem18  12602  ctiunctlemu1st  12676  ctiunctlemu2nd  12677  ctiunctlemudc  12679  ctiunctlemfo  12681  infpn2  12698  issgrp  13105  ismnddef  13120  gsumvallem2  13195  isgrp  13208  elnmz  13414  iscmn  13499  isrng  13566  issrg  13597  isring  13632  iscrng  13635  isnzr  13813  islring  13824  isrrg  13895  isdomn  13901  islmod  13923  psrbag  14299  psr1clfi  14316  isxms  14771  isms  14773  ivthinclemlm  14954  ivthinclemum  14955  ivthinclemlopn  14956  ivthinclemlr  14957  ivthinclemuopn  14958  ivthinclemur  14959  ivthinclemdisj  14960  ivthinclemloc  14961  mpodvdsmulf1o  15310  lgslem2  15326  lgslem3  15327  lgsfcl2  15331  0nninf  15735  nnsf  15736  peano4nninf  15737  nninfalllem1  15739  nninfself  15744  qdencn  15758