Theorem eleqtrdi 2331

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

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

Assertion

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

Proof of Theorem eleqtrdi

Step	Hyp	Ref	Expression
1		eleqtrdi.1	. 2 |- ( ph -> A e. B )
2		eleqtrdi.2	. . 3 |- B = C
3	2	a1i 9	. 2 |- ( ph -> B = C )
4	1, 3	eleqtrd 2317	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:  eleqtrrdi  2332  prid2g  3816  freccllem  6677  2omap  7324  nninfisol  7479  finomni  7486  exmidomniim  7487  ismkvnex  7501  exmidaclem  7570  pw1m  7589  caucvgprprlem2  8083  gt0srpr  8121  indfdc  9307  eluzel2  9942  fseq1p1m1  10518  fznn0sub2  10552  nn0split  10560  nnsplit  10561  exple1  11053  bcval5  11223  bcpasc  11226  hashf1  11309  zfz1isolemsplit  11312  seq3coll  11316  ccatrn  11399  swrdccat2  11465  cats1un  11515  pfxccatin12lem3  11526  cats1fvd  11560  clim2ser  12128  clim2ser2  12129  iserex  12130  isermulc2  12131  iserle  12133  iserge0  12134  climub  12135  climserle  12136  serf0  12143  summodclem3  12172  summodclem2a  12173  fsum3  12179  sum0  12180  fsumcl2lem  12190  fsumadd  12198  isumclim3  12215  isumadd  12223  fsump1i  12225  fsummulc2  12240  cvgcmpub  12268  binom1dif  12279  isumshft  12282  isumsplit  12283  isumrpcl  12286  arisum2  12291  trireciplem  12292  geoserap  12299  geolim  12303  geo2lim  12308  cvgratnnlemnexp  12316  cvgratnnlemseq  12318  cvgratgt0  12325  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  clim2prod  12331  clim2divap  12332  prodmodclem3  12367  prodmodclem2a  12368  fprodseq  12375  fprodntrivap  12376  fprodssdc  12382  fprodmul  12383  fprodabs  12408  fprodeq0  12409  efcvgfsum  12459  efcj  12465  effsumlt  12484  mod2eq1n2dvds  12671  bitsfzolem  12746  bitsfzo  12747  bitsfi  12749  bitsinv1lem  12753  bitsinv1  12754  nninfctlemfo  12842  algrp1  12849  phiprmpw  13029  crth  13031  phimullem  13032  prmdiv  13042  pcpremul  13101  pcmpt  13151  pcfac  13158  pockthlem  13164  pockthg  13165  1arith  13175  ballotfilem2  13286  ballotfilemfrceq  13330  ennnfonelemp1  13355  nninfdclemp1  13399  relelbasov  13474  gzsumwsubmcl  13860  gzsumwmhm  13862  mulgnnp1  13992  mulgnn0z  14011  mulgnndir  14013  gsump1  14247  idomdomd  14695  idomcringd  14696  lspprid2  14858  istps  15258  topontopn  15263  cldrcl  15328  cnrehmeocntop  15836  elplyd  15967  ply1termlem  15968  ply1term  15969  plyaddlem1  15973  plymullem1  15974  plyaddlem  15975  plymullem  15976  plycoeid3  15983  plycolemc  15984  plycj  15987  dvply1  15991  birthdaylem2  16226  birthdaylem3  16227  ppiprm  16259  ppinprm  16260  chtprm  16261  chtnprm  16262  0sgmppw  16287  1sgmprm  16288  ppiublem2  16292  chtublem  16295  bposlem5  16315  lgsval2lem  16334  lgsdir2lem3  16354  lgsdir2lem5  16356  lgsdir  16359  lgsdilem2  16360  lgsdi  16361  lgsne0  16362  gausslemma2dlem3  16387  lgseisenlem1  16394  lgseisenlem4  16397  lgsquadlem2  16402  umgrpredgv  16593  subgruhgredgdm  16716  eupth2lemsfi  16924  depindlem1  16952  nnsf  17254  nninfsellemqall  17264  nninfomnilem  17267  nnnninfex  17271  nninfnfiinf  17272  cvgcmp2nlemabs  17287  trilpolemeq1  17296  nconstwlpolemgt0  17321