Theorem elrab2 2896

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 2244	. 2 |- ( A e. C <-> A e. { x e. B | ph } )
3		elrab2.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elrab 2893	. 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 1353   e. wcel 2148   {crab 2459

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-v 2739

This theorem is referenced by:  elrabsf  3001  pwnss  4156  regexmidlemm  4528  regexmidlem1  4529  reg2exmidlema  4530  tfis  4579  ctssdccl  7104  nninff  7115  infnninf  7116  infnninfOLD  7117  nnnninf  7118  nnnninfeq  7120  nnnninfeq2  7121  nninfwlpoimlemg  7167  exmidaclem  7201  ltexprlemell  7585  ltexprlemelu  7586  cauappcvgprlemm  7632  cauappcvgprlemopl  7633  cauappcvgprlemlol  7634  cauappcvgprlemopu  7635  cauappcvgprlemupu  7636  cauappcvgprlemdisj  7638  cauappcvgprlemloc  7639  cauappcvgprlemladdfu  7641  cauappcvgprlemladdfl  7642  cauappcvgprlemladdru  7643  cauappcvgprlemladdrl  7644  cauappcvgprlem2  7647  caucvgprlemm  7655  caucvgprlemopl  7656  caucvgprlemlol  7657  caucvgprlemopu  7658  caucvgprlemupu  7659  caucvgprlemdisj  7661  caucvgprlemloc  7662  caucvgprlemladdfu  7664  caucvgprlem2  7667  caucvgprprlemell  7672  caucvgprprlemelu  7673  caucvgprprlemml  7681  caucvgprprlemmu  7682  caucvgprprlemexbt  7693  caucvgprprlem2  7697  suplocsrlemb  7793  suplocsrlempr  7794  suplocsrlem  7795  axpre-suploclemres  7888  elz  9241  elrp  9639  repos  9954  zsupssdc  11935  isprm  12089  oddpwdc  12154  sqpweven  12155  2sqpwodd  12156  phimullem  12205  eulerthlem1  12207  eulerthlemfi  12208  eulerthlemrprm  12209  eulerthlemth  12212  hashgcdlem  12218  pclem0  12266  pclemub  12267  pclemdc  12268  pcprecl  12269  pcprendvds  12270  1arith  12345  elgz  12349  ctiunctlemu1st  12415  ctiunctlemu2nd  12416  ctiunctlemudc  12418  ctiunctlemfo  12420  infpn2  12437  issgrp  12698  ismnddef  12708  isgrp  12770  iscmn  12920  issrg  12971  isring  13006  iscrng  13009  isxms  13611  isms  13613  ivthinclemlm  13772  ivthinclemum  13773  ivthinclemlopn  13774  ivthinclemlr  13775  ivthinclemuopn  13776  ivthinclemur  13777  ivthinclemdisj  13778  ivthinclemloc  13779  lgslem2  14062  lgslem3  14063  lgsfcl2  14067  0nninf  14402  nnsf  14403  peano4nninf  14404  nninfalllem1  14406  nninfself  14411  qdencn  14424