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  7289  nninff  7300  nninfninc  7301  infnninf  7302  infnninfOLD  7303  nnnninf  7304  nnnninfeq  7306  nnnninfeq2  7307  nninfwlpoimlemg  7353  exmidaclem  7401  ltexprlemell  7796  ltexprlemelu  7797  cauappcvgprlemm  7843  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemopu  7846  cauappcvgprlemupu  7847  cauappcvgprlemdisj  7849  cauappcvgprlemloc  7850  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  cauappcvgprlem2  7858  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemopu  7869  caucvgprlemupu  7870  caucvgprlemdisj  7872  caucvgprlemloc  7873  caucvgprlemladdfu  7875  caucvgprlem2  7878  caucvgprprlemell  7883  caucvgprprlemelu  7884  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemexbt  7904  caucvgprprlem2  7908  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  axpre-suploclemres  8099  elz  9459  elrp  9863  repos  10178  zsupssdc  10470  bitsfzolem  12481  isprm  12647  oddpwdc  12712  sqpweven  12713  2sqpwodd  12714  phimullem  12763  eulerthlem1  12765  eulerthlemfi  12766  eulerthlemrprm  12767  eulerthlemth  12770  hashgcdlem  12776  pclem0  12825  pclemub  12826  pclemdc  12827  pcprecl  12828  pcprendvds  12829  1arith  12906  elgz  12910  4sqlem13m  12942  4sqlem17  12946  4sqlem18  12947  ctiunctlemu1st  13021  ctiunctlemu2nd  13022  ctiunctlemudc  13024  ctiunctlemfo  13026  infpn2  13043  issgrp  13452  ismnddef  13467  gsumvallem2  13542  isgrp  13555  elnmz  13761  iscmn  13846  isrng  13913  issrg  13944  isring  13979  iscrng  13982  isnzr  14161  islring  14172  isrrg  14243  isdomn  14249  islmod  14271  psrbag  14649  psr1clfi  14668  isxms  15141  isms  15143  ivthinclemlm  15324  ivthinclemum  15325  ivthinclemlopn  15326  ivthinclemlr  15327  ivthinclemuopn  15328  ivthinclemur  15329  ivthinclemdisj  15330  ivthinclemloc  15331  mpodvdsmulf1o  15680  lgslem2  15696  lgslem3  15697  lgsfcl2  15701  lfgredg2dom  15946  uspgredg2vlem  16034  uspgredg2v  16035  usgredg2vlem1  16036  usgredg2vlem2  16037  ushgredgedg  16040  ushgredgedgloop  16042  0nninf  16458  nnsf  16459  peano4nninf  16460  nninfalllem1  16462  nninfself  16467  qdencn  16483