Theorem eleqtrrdi 2332

Description: A membership and equality inference. (Contributed by NM, 24-Apr-2005.)

Hypotheses

Ref	Expression
eleqtrrdi.1	|- ( ph -> A e. B )
eleqtrrdi.2	|- C = B

Assertion

Ref	Expression
eleqtrrdi	|- ( ph -> A e. C )

Proof of Theorem eleqtrrdi

Step	Hyp	Ref	Expression
1		eleqtrrdi.1	. 2 |- ( ph -> A e. B )
2		eleqtrrdi.2	. . 3 |- C = B
3	2	eqcomi 2242	. 2 |- B = C
4	1, 3	eleqtrdi 2331	1 |- ( ph -> A e. C )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  brelrng  5013  elabrex  5963  elabrexg  5964  fliftel1  6000  ovidig  6206  unielxp  6408  2oconcl  6712  ecopqsi  6864  eroprf  6902  exmidpweq  7216  sbthlem2  7275  djulclr  7389  djurclr  7390  djulcl  7391  djurcl  7392  caseinl  7431  caseinr  7432  ctssdccl  7451  isnumi  7527  addclnq  7742  mulclnq  7743  recexnq  7757  ltexnqq  7775  prarloclemarch  7785  prarloclemarch2  7786  nnnq  7789  nqnq0  7808  addclnq0  7818  mulclnq0  7819  nqpnq0nq  7820  prarloclemlt  7860  prarloclemlo  7861  prarloclemcalc  7869  nqprm  7909  cauappcvgprlem2  8027  caucvgprlem2  8047  addclsr  8120  mulclsr  8121  prsrcl  8151  mappsrprg  8171  suplocsrlemb  8173  pitonnlem2  8214  pitore  8217  recnnre  8218  axaddcl  8231  axmulcl  8233  axcaucvglemcl  8262  axcaucvglemval  8264  axcaucvglemcau  8265  axcaucvglemres  8266  uztrn2  9940  eluz2nn  9966  peano2uzs  9984  rebtwn2z  10689  seqf  10901  ser0  10970  bcm1k  11198  bcp1nk  11200  bcpasc  11204  hashennn  11219  hashcl  11220  climconst  12056  climshft2  12072  clim2ser  12103  clim2ser2  12104  iserex  12105  serf0  12118  zsumdc  12151  fsump1i  12200  iserabs  12242  isumshft  12257  isumsplit  12258  isum1p  12259  isumrpcl  12261  cvgratnnlemseq  12293  cvgratz  12299  cvgratgt0  12300  clim2prod  12306  clim2divap  12307  prodf1  12309  ntrivcvgap0  12316  zproddc  12346  fprodntrivap  12351  fprodabs  12383  fprodeq0  12384  ef0lem  12427  dvdsflip  12618  fzo0dvdseq  12624  bitsinv1  12729  gcdsupcl  12735  nninfctlemfo  12817  ialgr0  12822  prmind2  12898  crth  13002  prmdiv  13013  pockthlem  13135  pockthg  13136  prmunb  13141  ennnfonelemkh  13303  ennnfonelemrn  13310  ennnfonelemdm  13311  ctiunctlemf  13329  strslfv2d  13395  bassetsnn  13409  1strbas  13471  2strbasg  13474  2stropg  13475  2strbas1g  13477  rngbaseg  13490  rngplusgg  13491  rngmulrg  13492  srngbased  13501  srngplusgd  13502  srngmulrd  13503  srnginvld  13504  lmodbased  13519  lmodplusgd  13520  lmodscad  13521  lmodvscad  13522  ipsbased  13531  ipsaddgd  13532  ipsmulrd  13533  ipsscad  13534  ipsvscad  13535  ipsipd  13536  topgrpbasd  13551  topgrpplusgd  13552  topgrptsetd  13553  mulgnnp1  13933  znf1o  14986  lmconst  15317  lmss  15347  uptx  15375  cnmpt1res  15397  dvidlemap  15792  dvidrelem  15793  dvrecap  15814  plycolemc  15859  plycn  15863  pilem3  15884  logbleb  16063  logblt  16064  lgseisenlem1  16189  structvtxval  16280  ushgredgedgloop  16469  subgruhgredgdm  16511  wlkvtxm  16581  wlk1walkdom  16600  depindlem2  16748  djulclALT  16829  djurclALT  16830  pwle2  17028  trilpolemeq1  17089