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  4159  regexmidlemm  4531  regexmidlem1  4532  reg2exmidlema  4533  tfis  4582  ctssdccl  7109  nninff  7120  infnninf  7121  infnninfOLD  7122  nnnninf  7123  nnnninfeq  7125  nnnninfeq2  7126  nninfwlpoimlemg  7172  exmidaclem  7206  ltexprlemell  7596  ltexprlemelu  7597  cauappcvgprlemm  7643  cauappcvgprlemopl  7644  cauappcvgprlemlol  7645  cauappcvgprlemopu  7646  cauappcvgprlemupu  7647  cauappcvgprlemdisj  7649  cauappcvgprlemloc  7650  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  cauappcvgprlem2  7658  caucvgprlemm  7666  caucvgprlemopl  7667  caucvgprlemlol  7668  caucvgprlemopu  7669  caucvgprlemupu  7670  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlemladdfu  7675  caucvgprlem2  7678  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemml  7692  caucvgprprlemmu  7693  caucvgprprlemexbt  7704  caucvgprprlem2  7708  suplocsrlemb  7804  suplocsrlempr  7805  suplocsrlem  7806  axpre-suploclemres  7899  elz  9254  elrp  9654  repos  9969  zsupssdc  11954  isprm  12108  oddpwdc  12173  sqpweven  12174  2sqpwodd  12175  phimullem  12224  eulerthlem1  12226  eulerthlemfi  12227  eulerthlemrprm  12228  eulerthlemth  12231  hashgcdlem  12237  pclem0  12285  pclemub  12286  pclemdc  12287  pcprecl  12288  pcprendvds  12289  1arith  12364  elgz  12368  ctiunctlemu1st  12434  ctiunctlemu2nd  12435  ctiunctlemudc  12437  ctiunctlemfo  12439  infpn2  12456  issgrp  12808  ismnddef  12818  isgrp  12882  elnmz  13066  iscmn  13094  issrg  13146  isring  13181  iscrng  13184  isnzr  13323  islring  13331  islmod  13379  isxms  13921  isms  13923  ivthinclemlm  14082  ivthinclemum  14083  ivthinclemlopn  14084  ivthinclemlr  14085  ivthinclemuopn  14086  ivthinclemur  14087  ivthinclemdisj  14088  ivthinclemloc  14089  lgslem2  14372  lgslem3  14373  lgsfcl2  14377  0nninf  14723  nnsf  14724  peano4nninf  14725  nninfalllem1  14727  nninfself  14732  qdencn  14745