Theorem eleqtrdi 2327

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 2313	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2205

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-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  eleqtrrdi  2328  prid2g  3801  freccllem  6646  2omap  7282  nninfisol  7437  finomni  7444  exmidomniim  7445  ismkvnex  7459  exmidaclem  7528  pw1m  7547  caucvgprprlem2  8041  gt0srpr  8079  eluzel2  9876  fseq1p1m1  10450  fznn0sub2  10484  nn0split  10492  nnsplit  10493  exple1  10981  bcval5  11150  bcpasc  11153  zfz1isolemsplit  11235  seq3coll  11239  ccatrn  11322  swrdccat2  11388  cats1un  11438  pfxccatin12lem3  11449  cats1fvd  11483  clim2ser  12047  clim2ser2  12048  iserex  12049  isermulc2  12050  iserle  12052  iserge0  12053  climub  12054  climserle  12055  serf0  12062  summodclem3  12091  summodclem2a  12092  fsum3  12098  sum0  12099  fsumcl2lem  12109  fsumadd  12117  isumclim3  12134  isumadd  12142  fsump1i  12144  fsummulc2  12159  cvgcmpub  12187  binom1dif  12198  isumshft  12201  isumsplit  12202  isumrpcl  12205  arisum2  12210  trireciplem  12211  geoserap  12218  geolim  12222  geo2lim  12227  cvgratnnlemnexp  12235  cvgratnnlemseq  12237  cvgratgt0  12244  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  clim2prod  12250  clim2divap  12251  prodmodclem3  12286  prodmodclem2a  12287  fprodseq  12294  fprodntrivap  12295  fprodssdc  12301  fprodmul  12302  fprodabs  12327  fprodeq0  12328  efcvgfsum  12378  efcj  12384  effsumlt  12403  mod2eq1n2dvds  12590  bitsfzolem  12665  bitsfzo  12666  bitsfi  12668  bitsinv1lem  12672  bitsinv1  12673  nninfctlemfo  12761  algrp1  12768  phiprmpw  12944  crth  12946  phimullem  12947  prmdiv  12957  pcpremul  13016  pcmpt  13066  pcfac  13073  pockthlem  13079  pockthg  13080  1arith  13090  ballotfilem2  13172  ballotfilemfrceq  13216  ennnfonelemp1  13241  nninfdclemp1  13285  relelbasov  13359  gsumwsubmcl  13751  gsumwmhm  13753  mulgnnp1  13883  mulgnn0z  13902  mulgnndir  13904  gfsump1  14108  idomdomd  14524  idomcringd  14525  lspprid2  14686  istps  15023  topontopn  15028  cldrcl  15093  cnrehmeocntop  15601  elplyd  15732  ply1termlem  15733  ply1term  15734  plyaddlem1  15738  plymullem1  15739  plyaddlem  15740  plymullem  15741  plycoeid3  15748  plycolemc  15749  plycj  15752  dvply1  15756  0sgmppw  15987  1sgmprm  15988  lgsval2lem  16009  lgsdir2lem3  16029  lgsdir2lem5  16031  lgsdir  16034  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  gausslemma2dlem3  16062  lgseisenlem1  16069  lgseisenlem4  16072  lgsquadlem2  16077  umgrpredgv  16268  subgruhgredgdm  16391  eupth2lemsfi  16599  depindlem1  16627  nnsf  16909  nninfsellemqall  16919  nninfomnilem  16922  nnnninfex  16926  nninfnfiinf  16927  cvgcmp2nlemabs  16942  trilpolemeq1  16950  nconstwlpolemgt0  16976