Theorem elrab2 2985

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   e. wcel 2209   {crab 2532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-v 2823

This theorem is used by:  elrabsf  3090  pwnss  4298  regexmidlemm  4681  regexmidlem1  4682  reg2exmidlema  4683  tfis  4732  ctssdccl  7457  nninff  7468  nninfninc  7469  infnninf  7470  infnninfOLD  7471  nnnninf  7472  nnnninfeq  7474  nnnninfeq2  7475  nninfwlpoimlemg  7521  exmidaclem  7570  ltexprlemell  7971  ltexprlemelu  7972  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemopu  8021  cauappcvgprlemupu  8022  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem2  8033  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemopu  8044  caucvgprlemupu  8045  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemladdfu  8050  caucvgprlem2  8053  caucvgprprlemell  8058  caucvgprprlemelu  8059  caucvgprprlemml  8067  caucvgprprlemmu  8068  caucvgprprlemexbt  8079  caucvgprprlem2  8083  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  axpre-suploclemres  8274  elz  9655  elrp  10072  repos  10388  zsupssdc  10689  bitsfzolem  12745  isprm  12911  nnmaxpw  12977  sqpweven  12979  2sqpwodd  12980  phimullem  13031  eulerthlem1  13033  eulerthlemfi  13034  eulerthlemrprm  13035  eulerthlemth  13038  hashgcdlem  13044  pclem0  13093  pclemub  13094  pclemdc  13095  pcprecl  13096  pcprendvds  13097  1arith  13174  elgz  13178  4sqlem13m  13210  4sqlem17  13214  4sqlem18  13215  ballotfilemelo  13279  ballotfileme  13293  ballotfilemscl  13304  ctiunctlemu1st  13382  ctiunctlemu2nd  13383  ctiunctlemudc  13385  ctiunctlemfo  13387  infpn2  13404  issgrp  13776  ismnddef  13789  gsumvallem2  13858  isgrp  13869  elnmz  14069  iscmn  14185  isrng  14339  issrg  14375  isring  14410  iscrng  14413  isnzr  14596  islring  14607  isrrg  14679  isdomn  14686  isdrngtap  14714  islmod  14735  isassa  15110  psrbag  15163  psrbagconcl  15176  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  gsumbagdiaglem  15184  psr1clfi  15207  mplelbas  15224  isxms  15694  isms  15696  ivthinclemlm  15877  ivthinclemum  15878  ivthinclemlopn  15879  ivthinclemlr  15880  ivthinclemuopn  15881  ivthinclemur  15882  ivthinclemdisj  15883  ivthinclemloc  15884  zprmlogbaplem3  16234  mpodvdsmulf1o  16301  lgslem2  16342  lgslem3  16343  lgsfcl2  16347  lfgredg2dom  16595  uspgredg2vlem  16683  uspgredg2v  16684  usgredg2vlem1  16685  usgredg2vlem2  16686  ushgredgedg  16689  ushgredgedgloop  16691  isclwwlknon  16893  s2elclwwlknon2  16899  0nninf  17270  nnsf  17271  peano4nninf  17272  nninfalllem1  17274  nninfself  17279  qdencn  17295