Theorem elrab2 2962

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 2296	. 2 |- ( A e. C <-> A e. { x e. B | ph } )
3		elrab2.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elrab 2959	. 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 1395   e. wcel 2200   {crab 2512

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-v 2801

This theorem is referenced by:  elrabsf  3067  pwnss  4243  regexmidlemm  4624  regexmidlem1  4625  reg2exmidlema  4626  tfis  4675  ctssdccl  7278  nninff  7289  nninfninc  7290  infnninf  7291  infnninfOLD  7292  nnnninf  7293  nnnninfeq  7295  nnnninfeq2  7296  nninfwlpoimlemg  7342  exmidaclem  7390  ltexprlemell  7785  ltexprlemelu  7786  cauappcvgprlemm  7832  cauappcvgprlemopl  7833  cauappcvgprlemlol  7834  cauappcvgprlemopu  7835  cauappcvgprlemupu  7836  cauappcvgprlemdisj  7838  cauappcvgprlemloc  7839  cauappcvgprlemladdfu  7841  cauappcvgprlemladdfl  7842  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  cauappcvgprlem2  7847  caucvgprlemm  7855  caucvgprlemopl  7856  caucvgprlemlol  7857  caucvgprlemopu  7858  caucvgprlemupu  7859  caucvgprlemdisj  7861  caucvgprlemloc  7862  caucvgprlemladdfu  7864  caucvgprlem2  7867  caucvgprprlemell  7872  caucvgprprlemelu  7873  caucvgprprlemml  7881  caucvgprprlemmu  7882  caucvgprprlemexbt  7893  caucvgprprlem2  7897  suplocsrlemb  7993  suplocsrlempr  7994  suplocsrlem  7995  axpre-suploclemres  8088  elz  9448  elrp  9851  repos  10166  zsupssdc  10458  bitsfzolem  12465  isprm  12631  oddpwdc  12696  sqpweven  12697  2sqpwodd  12698  phimullem  12747  eulerthlem1  12749  eulerthlemfi  12750  eulerthlemrprm  12751  eulerthlemth  12754  hashgcdlem  12760  pclem0  12809  pclemub  12810  pclemdc  12811  pcprecl  12812  pcprendvds  12813  1arith  12890  elgz  12894  4sqlem13m  12926  4sqlem17  12930  4sqlem18  12931  ctiunctlemu1st  13005  ctiunctlemu2nd  13006  ctiunctlemudc  13008  ctiunctlemfo  13010  infpn2  13027  issgrp  13436  ismnddef  13451  gsumvallem2  13526  isgrp  13539  elnmz  13745  iscmn  13830  isrng  13897  issrg  13928  isring  13963  iscrng  13966  isnzr  14145  islring  14156  isrrg  14227  isdomn  14233  islmod  14255  psrbag  14633  psr1clfi  14652  isxms  15125  isms  15127  ivthinclemlm  15308  ivthinclemum  15309  ivthinclemlopn  15310  ivthinclemlr  15311  ivthinclemuopn  15312  ivthinclemur  15313  ivthinclemdisj  15314  ivthinclemloc  15315  mpodvdsmulf1o  15664  lgslem2  15680  lgslem3  15681  lgsfcl2  15685  lfgredg2dom  15930  uspgredg2vlem  16018  uspgredg2v  16019  usgredg2vlem1  16020  usgredg2vlem2  16021  ushgredgedg  16024  ushgredgedgloop  16026  0nninf  16370  nnsf  16371  peano4nninf  16372  nninfalllem1  16374  nninfself  16379  qdencn  16395