Theorem elrab2 2920

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 2260	. 2 |- ( A e. C <-> A e. { x e. B | ph } )
3		elrab2.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elrab 2917	. 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 1364   e. wcel 2164   {crab 2476

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rab 2481  df-v 2762

This theorem is referenced by:  elrabsf  3025  pwnss  4189  regexmidlemm  4565  regexmidlem1  4566  reg2exmidlema  4567  tfis  4616  ctssdccl  7172  nninff  7183  nninfninc  7184  infnninf  7185  infnninfOLD  7186  nnnninf  7187  nnnninfeq  7189  nnnninfeq2  7190  nninfwlpoimlemg  7236  exmidaclem  7270  ltexprlemell  7660  ltexprlemelu  7661  cauappcvgprlemm  7707  cauappcvgprlemopl  7708  cauappcvgprlemlol  7709  cauappcvgprlemopu  7710  cauappcvgprlemupu  7711  cauappcvgprlemdisj  7713  cauappcvgprlemloc  7714  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgprlem2  7722  caucvgprlemm  7730  caucvgprlemopl  7731  caucvgprlemlol  7732  caucvgprlemopu  7733  caucvgprlemupu  7734  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemladdfu  7739  caucvgprlem2  7742  caucvgprprlemell  7747  caucvgprprlemelu  7748  caucvgprprlemml  7756  caucvgprprlemmu  7757  caucvgprprlemexbt  7768  caucvgprprlem2  7772  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  axpre-suploclemres  7963  elz  9322  elrp  9724  repos  10039  zsupssdc  12094  isprm  12250  oddpwdc  12315  sqpweven  12316  2sqpwodd  12317  phimullem  12366  eulerthlem1  12368  eulerthlemfi  12369  eulerthlemrprm  12370  eulerthlemth  12373  hashgcdlem  12379  pclem0  12427  pclemub  12428  pclemdc  12429  pcprecl  12430  pcprendvds  12431  1arith  12508  elgz  12512  4sqlem13m  12544  4sqlem17  12548  4sqlem18  12549  ctiunctlemu1st  12594  ctiunctlemu2nd  12595  ctiunctlemudc  12597  ctiunctlemfo  12599  infpn2  12616  issgrp  12989  ismnddef  13002  gsumvallem2  13068  isgrp  13081  elnmz  13281  iscmn  13366  isrng  13433  issrg  13464  isring  13499  iscrng  13502  isnzr  13680  islring  13691  isrrg  13762  isdomn  13768  islmod  13790  psrbag  14166  isxms  14630  isms  14632  ivthinclemlm  14813  ivthinclemum  14814  ivthinclemlopn  14815  ivthinclemlr  14816  ivthinclemuopn  14817  ivthinclemur  14818  ivthinclemdisj  14819  ivthinclemloc  14820  lgslem2  15158  lgslem3  15159  lgsfcl2  15163  0nninf  15564  nnsf  15565  peano4nninf  15566  nninfalllem1  15568  nninfself  15573  qdencn  15587