Theorem eqeltrid 2283

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

Hypotheses

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

Assertion

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

Proof of Theorem eqeltrid

Step	Hyp	Ref	Expression
1		eqeltrid.1	. . 3 |- A = B
2	1	a1i 9	. 2 |- ( ph -> A = B )
3		eqeltrid.2	. 2 |- ( ph -> B e. C )
4	2, 3	eqeltrd 2273	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eqeltrrid  2284  csbexga  4162  rabexd  4179  otexg  4264  tpexg  4480  dmresexg  4970  f1oabexg  5519  funfvex  5578  riotaexg  5884  riotaprop  5904  fnovex  5958  ovexg  5959  fovcdm  6070  fnovrn  6075  cofunexg  6175  cofunex2g  6176  abrexex2g  6186  xpexgALT  6199  mpofvex  6272  tfrex  6435  frec0g  6464  freccllem  6469  ecexg  6605  qsexg  6659  pmex  6721  elixpsn  6803  diffifi  6964  unfidisj  6992  prfidisj  6997  tpfidisj  6999  tpfidceq  7000  ssfirab  7006  ssfidc  7007  fnfi  7011  funrnfi  7017  iunfidisj  7021  infclti  7098  supex2g  7108  infex2g  7109  djuex  7118  ctssdccl  7186  addvalex  7928  negcl  8243  intqfrac2  10428  intfracq  10429  frec2uzzd  10509  frecuzrdgrrn  10517  iseqf1olemqpcl  10618  seq3f1olemqsum  10622  seqf1oglem1  10628  seqf1oglem2  10629  bcval5  10872  xrmaxiflemval  11432  climmpt  11482  reccn2ap  11495  zsumdc  11566  fsumzcl2  11587  fsump1i  11615  fsumabs  11647  hash2iun1dif1  11662  mertenslemi1  11717  fprodcllemf  11795  bitsfzolem  12136  nninfctlemfo  12232  algrf  12238  algcvg  12241  algcvga  12244  algfx  12245  eucalgcvga  12251  eucalg  12252  crth  12417  phimullem  12418  eulerthlemth  12425  prmdiv  12428  pythagtriplem11  12468  pythagtriplem13  12470  pcprecl  12483  infpnlem1  12553  infpnlem2  12554  4sqlem5  12576  mul4sqlem  12587  4sqlemafi  12589  4sqlem13m  12597  4sqlem14  12598  4sqlem17  12601  4sqlem18  12602  ennnfonelemj0  12643  ennnfonelemom  12650  ressbasid  12773  ressval3d  12775  1strbas  12820  2strbasg  12822  2stropg  12823  restid  12952  topnvalg  12953  topnidg  12954  prdsval  12975  prdsplusg  12979  prdsmulr  12980  pwsval  12993  pwselbasb  12995  pwssnf1o  13000  imasival  13008  imasmulr  13011  imasaddfn  13019  imasaddval  13020  imasaddf  13021  imasmulfn  13022  imasmulval  13023  imasmulf  13024  qusval  13025  qusaddval  13037  qusaddf  13038  qusmulval  13039  qusmulf  13040  xpsval  13054  plusffvalg  13064  plusfvalg  13065  grpidvalg  13075  igsumvalx  13091  gsumfzval  13093  gsum0g  13098  gsumsplit1r  13100  gsumprval  13101  prdssgrpd  13117  issubmnd  13144  ress0g  13145  ismhm  13163  0mhm  13188  grpinvfvalg  13244  grpinvval  13245  grpinvfng  13246  grpsubfvalg  13247  grpsubval  13248  grpressid  13263  grplactfval  13303  prdsinvlem  13310  mulgfvalg  13327  mulgval  13328  mulgfng  13330  mulgnngsum  13333  mulgnnp1  13336  mulgnndir  13357  issubg  13379  subggrp  13383  issubg2m  13395  eqgfval  13428  eqgen  13433  quselbasg  13436  quseccl0g  13437  isghm  13449  ghmima  13471  ablressid  13541  gsumfzmptfidmadd  13545  mgpvalg  13555  mgpplusgg  13556  mgptopng  13561  mgpress  13563  rngressid  13586  issrg  13597  ringidss  13661  ring1  13691  ringressid  13695  opprvalg  13701  opprmulfvalg  13702  rdivmuldivd  13776  isnzr2  13816  issubrg  13853  subrgring  13856  rrgval  13894  islmod  13923  scaffvalg  13938  scafvalg  13939  lsssetm  13988  islssm  13989  islssmg  13990  lss1d  14015  lspfval  14020  lspval  14022  lspcl  14023  ellspsn  14049  rnglidlmmgm  14128  rnglidlmsgrp  14129  2idlval  14134  2idlvalg  14135  qusrhm  14160  zlmval  14259  zlmvscag  14265  znval  14268  znle  14269  znbaslemnn  14271  znbas  14276  znzrhval  14279  znleval  14285  psrval  14296  psrbasg  14303  psrelbas  14304  psrplusgg  14306  topopn  14328  topcld  14429  uncld  14433  iuncld  14435  unicld  14436  tgrest  14489  restin  14496  cnco  14541  cnrest  14555  cnptoprest2  14560  lmss  14566  txbasval  14587  txcn  14595  cnmpt12f  14606  hmeoco  14636  idhmeo  14637  blres  14754  metrest  14826  qtopbasss  14841  tgqioo  14875  divcnap  14885  fsumcncntop  14887  cncfmet  14912  sub1cncf  14922  sub2cncf  14923  cdivcncfap  14924  cnrehmeocntop  14930  cnplimcim  14987  limccnpcntop  14995  limccnp2lem  14996  limccnp2cntop  14997  dvfvalap  15001  dvidsslem  15013  dvmptfsum  15045  plyid  15066  fsumdvdsmul  15311  gausslemma2dlem0b  15375  gausslemma2dlem0d  15377  gausslemma2dlem0h  15381  gausslemma2dlem5a  15390  gausslemma2dlem5  15391  gausslemma2dlem6  15392  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisenlem4  15398  2lgslem2  15417  2sqlem8  15448  bj-snexg  15642  trilpolemcl  15768