Theorem eleqtrdi 2324

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

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

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

This theorem is referenced by:  eleqtrrdi  2325  prid2g  3776  freccllem  6568  nninfisol  7332  finomni  7339  exmidomniim  7340  ismkvnex  7354  exmidaclem  7423  pw1m  7442  caucvgprprlem2  7930  gt0srpr  7968  eluzel2  9760  fseq1p1m1  10329  fznn0sub2  10363  nn0split  10371  nnsplit  10372  exple1  10858  bcval5  11026  bcpasc  11029  zfz1isolemsplit  11103  seq3coll  11107  ccatrn  11187  swrdccat2  11253  cats1un  11303  pfxccatin12lem3  11314  cats1fvd  11348  clim2ser  11899  clim2ser2  11900  iserex  11901  isermulc2  11902  iserle  11904  iserge0  11905  climub  11906  climserle  11907  serf0  11914  summodclem3  11943  summodclem2a  11944  fsum3  11950  sum0  11951  fsumcl2lem  11961  fsumadd  11969  isumclim3  11986  isumadd  11994  fsump1i  11996  fsummulc2  12011  cvgcmpub  12039  binom1dif  12050  isumshft  12053  isumsplit  12054  isumrpcl  12057  arisum2  12062  trireciplem  12063  geoserap  12070  geolim  12074  geo2lim  12079  cvgratnnlemnexp  12087  cvgratnnlemseq  12089  cvgratgt0  12096  mertenslemi1  12098  mertenslem2  12099  mertensabs  12100  clim2prod  12102  clim2divap  12103  prodmodclem3  12138  prodmodclem2a  12139  fprodseq  12146  fprodntrivap  12147  fprodssdc  12153  fprodmul  12154  fprodabs  12179  fprodeq0  12180  efcvgfsum  12230  efcj  12236  effsumlt  12255  mod2eq1n2dvds  12442  bitsfzolem  12517  bitsfzo  12518  bitsfi  12520  bitsinv1lem  12524  bitsinv1  12525  nninfctlemfo  12613  algrp1  12620  phiprmpw  12796  crth  12798  phimullem  12799  prmdiv  12809  pcpremul  12868  pcmpt  12918  pcfac  12925  pockthlem  12931  pockthg  12932  1arith  12942  ennnfonelemp1  13029  nninfdclemp1  13073  relelbasov  13147  gsumwsubmcl  13581  gsumwmhm  13583  mulgnnp1  13719  mulgnn0z  13738  mulgnndir  13740  idomdomd  14294  idomcringd  14295  lspprid2  14429  istps  14759  topontopn  14764  cldrcl  14829  cnrehmeocntop  15337  elplyd  15468  ply1termlem  15469  ply1term  15470  plyaddlem1  15474  plymullem1  15475  plyaddlem  15476  plymullem  15477  plycoeid3  15484  plycolemc  15485  plycj  15488  dvply1  15492  0sgmppw  15720  1sgmprm  15721  lgsval2lem  15742  lgsdir2lem3  15762  lgsdir2lem5  15764  lgsdir  15767  lgsdilem2  15768  lgsdi  15769  lgsne0  15770  gausslemma2dlem3  15795  lgseisenlem1  15802  lgseisenlem4  15805  lgsquadlem2  15810  umgrpredgv  16001  subgruhgredgdm  16124  eupth2lemsfi  16332  depindlem1  16346  2omap  16615  nnsf  16628  nninfsellemqall  16638  nninfomnilem  16641  nnnninfex  16645  nninfnfiinf  16646  cvgcmp2nlemabs  16657  trilpolemeq1  16665  nconstwlpolemgt0  16689  gfsump1  16707