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  4192  regexmidlemm  4568  regexmidlem1  4569  reg2exmidlema  4570  tfis  4619  ctssdccl  7177  nninff  7188  nninfninc  7189  infnninf  7190  infnninfOLD  7191  nnnninf  7192  nnnninfeq  7194  nnnninfeq2  7195  nninfwlpoimlemg  7241  exmidaclem  7275  ltexprlemell  7665  ltexprlemelu  7666  cauappcvgprlemm  7712  cauappcvgprlemopl  7713  cauappcvgprlemlol  7714  cauappcvgprlemopu  7715  cauappcvgprlemupu  7716  cauappcvgprlemdisj  7718  cauappcvgprlemloc  7719  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlem2  7727  caucvgprlemm  7735  caucvgprlemopl  7736  caucvgprlemlol  7737  caucvgprlemopu  7738  caucvgprlemupu  7739  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprlemladdfu  7744  caucvgprlem2  7747  caucvgprprlemell  7752  caucvgprprlemelu  7753  caucvgprprlemml  7761  caucvgprprlemmu  7762  caucvgprprlemexbt  7773  caucvgprprlem2  7777  suplocsrlemb  7873  suplocsrlempr  7874  suplocsrlem  7875  axpre-suploclemres  7968  elz  9328  elrp  9730  repos  10045  zsupssdc  10328  bitsfzolem  12118  isprm  12277  oddpwdc  12342  sqpweven  12343  2sqpwodd  12344  phimullem  12393  eulerthlem1  12395  eulerthlemfi  12396  eulerthlemrprm  12397  eulerthlemth  12400  hashgcdlem  12406  pclem0  12455  pclemub  12456  pclemdc  12457  pcprecl  12458  pcprendvds  12459  1arith  12536  elgz  12540  4sqlem13m  12572  4sqlem17  12576  4sqlem18  12577  ctiunctlemu1st  12651  ctiunctlemu2nd  12652  ctiunctlemudc  12654  ctiunctlemfo  12656  infpn2  12673  issgrp  13046  ismnddef  13059  gsumvallem2  13125  isgrp  13138  elnmz  13338  iscmn  13423  isrng  13490  issrg  13521  isring  13556  iscrng  13559  isnzr  13737  islring  13748  isrrg  13819  isdomn  13825  islmod  13847  psrbag  14223  isxms  14687  isms  14689  ivthinclemlm  14870  ivthinclemum  14871  ivthinclemlopn  14872  ivthinclemlr  14873  ivthinclemuopn  14874  ivthinclemur  14875  ivthinclemdisj  14876  ivthinclemloc  14877  mpodvdsmulf1o  15226  lgslem2  15242  lgslem3  15243  lgsfcl2  15247  0nninf  15648  nnsf  15649  peano4nninf  15650  nninfalllem1  15652  nninfself  15657  qdencn  15671