Theorem elrab2 2889

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 2237	. 2 |- ( A e. C <-> A e. { x e. B | ph } )
3		elrab2.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elrab 2886	. 2 |- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )
5	2, 4	bitri 183	1 |- ( A e. C <-> ( A e. B /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1348   e. wcel 2141   {crab 2452

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rab 2457  df-v 2732

This theorem is referenced by:  elrabsf  2993  pwnss  4145  regexmidlemm  4516  regexmidlem1  4517  reg2exmidlema  4518  tfis  4567  ctssdccl  7088  nninff  7099  infnninf  7100  infnninfOLD  7101  nnnninf  7102  nnnninfeq  7104  nnnninfeq2  7105  nninfwlpoimlemg  7151  exmidaclem  7185  ltexprlemell  7560  ltexprlemelu  7561  cauappcvgprlemm  7607  cauappcvgprlemopl  7608  cauappcvgprlemlol  7609  cauappcvgprlemopu  7610  cauappcvgprlemupu  7611  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem2  7622  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemlol  7632  caucvgprlemopu  7633  caucvgprlemupu  7634  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlemladdfu  7639  caucvgprlem2  7642  caucvgprprlemell  7647  caucvgprprlemelu  7648  caucvgprprlemml  7656  caucvgprprlemmu  7657  caucvgprprlemexbt  7668  caucvgprprlem2  7672  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  axpre-suploclemres  7863  elz  9214  elrp  9612  repos  9927  zsupssdc  11909  isprm  12063  oddpwdc  12128  sqpweven  12129  2sqpwodd  12130  phimullem  12179  eulerthlem1  12181  eulerthlemfi  12182  eulerthlemrprm  12183  eulerthlemth  12186  hashgcdlem  12192  pclem0  12240  pclemub  12241  pclemdc  12242  pcprecl  12243  pcprendvds  12244  1arith  12319  elgz  12323  ctiunctlemu1st  12389  ctiunctlemu2nd  12390  ctiunctlemudc  12392  ctiunctlemfo  12394  infpn2  12411  issgrp  12644  ismnddef  12654  isgrp  12714  isxms  13245  isms  13247  ivthinclemlm  13406  ivthinclemum  13407  ivthinclemlopn  13408  ivthinclemlr  13409  ivthinclemuopn  13410  ivthinclemur  13411  ivthinclemdisj  13412  ivthinclemloc  13413  lgslem2  13696  lgslem3  13697  lgsfcl2  13701  0nninf  14037  nnsf  14038  peano4nninf  14039  nninfalllem1  14041  nninfself  14046  qdencn  14059