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 )

Syntax hints:   -> wi 4   = wceq 1402   e. wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

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

This theorem is referenced by:  eleqtrrdi  2332  prid2g  3812  freccllem  6663  2omap  7308  nninfisol  7463  finomni  7470  exmidomniim  7471  ismkvnex  7485  exmidaclem  7554  pw1m  7573  caucvgprprlem2  8067  gt0srpr  8105  eluzel2  9905  fseq1p1m1  10479  fznn0sub2  10513  nn0split  10521  nnsplit  10522  exple1  11010  bcval5  11179  bcpasc  11182  hashf1  11265  zfz1isolemsplit  11268  seq3coll  11272  ccatrn  11355  swrdccat2  11421  cats1un  11471  pfxccatin12lem3  11482  cats1fvd  11516  clim2ser  12081  clim2ser2  12082  iserex  12083  isermulc2  12084  iserle  12086  iserge0  12087  climub  12088  climserle  12089  serf0  12096  summodclem3  12125  summodclem2a  12126  fsum3  12132  sum0  12133  fsumcl2lem  12143  fsumadd  12151  isumclim3  12168  isumadd  12176  fsump1i  12178  fsummulc2  12193  cvgcmpub  12221  binom1dif  12232  isumshft  12235  isumsplit  12236  isumrpcl  12239  arisum2  12244  trireciplem  12245  geoserap  12252  geolim  12256  geo2lim  12261  cvgratnnlemnexp  12269  cvgratnnlemseq  12271  cvgratgt0  12278  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  clim2prod  12284  clim2divap  12285  prodmodclem3  12320  prodmodclem2a  12321  fprodseq  12328  fprodntrivap  12329  fprodssdc  12335  fprodmul  12336  fprodabs  12361  fprodeq0  12362  efcvgfsum  12412  efcj  12418  effsumlt  12437  mod2eq1n2dvds  12624  bitsfzolem  12699  bitsfzo  12700  bitsfi  12702  bitsinv1lem  12706  bitsinv1  12707  nninfctlemfo  12795  algrp1  12802  phiprmpw  12978  crth  12980  phimullem  12981  prmdiv  12991  pcpremul  13050  pcmpt  13100  pcfac  13107  pockthlem  13113  pockthg  13114  1arith  13124  ballotfilem2  13206  ballotfilemfrceq  13250  ennnfonelemp1  13275  nninfdclemp1  13319  relelbasov  13393  gzsumwsubmcl  13778  gzsumwmhm  13780  mulgnnp1  13910  mulgnn0z  13929  mulgnndir  13931  gsump1  14134  idomdomd  14559  idomcringd  14560  lspprid2  14721  istps  15056  topontopn  15061  cldrcl  15126  cnrehmeocntop  15634  elplyd  15765  ply1termlem  15766  ply1term  15767  plyaddlem1  15771  plymullem1  15772  plyaddlem  15773  plymullem  15774  plycoeid3  15781  plycolemc  15782  plycj  15785  dvply1  15789  0sgmppw  16021  1sgmprm  16022  lgsval2lem  16043  lgsdir2lem3  16063  lgsdir2lem5  16065  lgsdir  16068  lgsdilem2  16069  lgsdi  16070  lgsne0  16071  gausslemma2dlem3  16096  lgseisenlem1  16103  lgseisenlem4  16106  lgsquadlem2  16111  umgrpredgv  16302  subgruhgredgdm  16425  eupth2lemsfi  16633  depindlem1  16661  nnsf  16953  nninfsellemqall  16963  nninfomnilem  16966  nnnninfex  16970  nninfnfiinf  16971  cvgcmp2nlemabs  16986  trilpolemeq1  16994  nconstwlpolemgt0  17019