Theorem eqeltrid 2318

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

Hypotheses

Ref	Expression
eqeltrid.1	⊢ 𝐴 = 𝐵
eqeltrid.2	⊢ (𝜑 → 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
eqeltrid	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eqeltrid

Step	Hyp	Ref	Expression
1		eqeltrid.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqeltrid.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	2, 3	eqeltrd 2308	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1398   ∈ 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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

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

This theorem is referenced by:  eqeltrrid  2319  csbexga  4222  rabexd  4240  otexg  4328  tpexg  4547  dmresexg  5042  f1oabexg  5604  funfvex  5665  elfvfvex  5682  riotaexg  5985  riotaeqimp  6006  riotaprop  6007  fnovex  6061  ovexg  6062  elovimad  6072  fovcdm  6175  fnovrn  6180  cofunexg  6280  cofunex2g  6281  abrexex2g  6291  xpexgALT  6304  mpofvex  6379  mptsuppdifd  6433  tfrex  6577  frec0g  6606  freccllem  6611  ecexg  6749  qsexg  6803  pmex  6865  elixpsn  6947  diffifi  7126  unfidisj  7157  prfidisj  7162  tpfidisj  7164  tpfidceq  7165  ssfirab  7172  ssfidc  7173  fnfi  7178  funrnfi  7184  iunfidisj  7188  infclti  7282  supex2g  7292  infex2g  7293  djuex  7302  ctssdccl  7370  addvalex  8124  negcl  8438  intqfrac2  10644  intfracq  10645  frec2uzzd  10725  frecuzrdgrrn  10733  iseqf1olemqpcl  10834  seq3f1olemqsum  10838  seqf1oglem1  10844  seqf1oglem2  10845  bcval5  11088  swrdccatin2  11376  pfxccatin12lem2  11378  pfxccatin12  11380  pfxccat3  11381  pfxccatpfx2  11384  pfxccat3a  11385  swrdccat3blem  11386  swrdccat3b  11387  cats1cld  11410  xrmaxiflemval  11890  climmpt  11940  reccn2ap  11953  zsumdc  12025  fsumzcl2  12046  fsump1i  12074  fsumabs  12106  hash2iun1dif1  12121  mertenslemi1  12176  fprodcllemf  12254  bitsfzolem  12595  nninfctlemfo  12691  algrf  12697  algcvg  12700  algcvga  12703  algfx  12704  eucalgcvga  12710  eucalg  12711  crth  12876  phimullem  12877  eulerthlemth  12884  prmdiv  12887  pythagtriplem11  12927  pythagtriplem13  12929  pcprecl  12942  infpnlem1  13012  infpnlem2  13013  4sqlem5  13035  mul4sqlem  13046  4sqlemafi  13048  4sqlem13m  13056  4sqlem14  13057  4sqlem17  13060  4sqlem18  13061  ennnfonelemj0  13102  ennnfonelemom  13109  ressbasid  13233  ressval3d  13235  1strbas  13280  2strbasg  13283  2stropg  13284  restid  13413  topnvalg  13414  topnidg  13415  prdsval  13436  prdsplusg  13440  prdsmulr  13441  pwsval  13454  pwselbasb  13456  pwssnf1o  13461  imasival  13469  imasmulr  13472  imasaddfn  13480  imasaddval  13481  imasaddf  13482  imasmulfn  13483  imasmulval  13484  imasmulf  13485  qusval  13486  qusaddval  13498  qusaddf  13499  qusmulval  13500  qusmulf  13501  xpsval  13515  plusffvalg  13525  plusfvalg  13526  grpidvalg  13536  igsumvalx  13552  gsumfzval  13554  gsum0g  13559  gsumsplit1r  13561  gsumprval  13562  prdssgrpd  13578  issubmnd  13605  ress0g  13606  ismhm  13624  0mhm  13649  grpinvfvalg  13705  grpinvval  13706  grpinvfng  13707  grpsubfvalg  13708  grpsubval  13709  grpressid  13724  grplactfval  13764  prdsinvlem  13771  mulgfvalg  13788  mulgval  13789  mulgfng  13791  mulgnngsum  13794  mulgnnp1  13797  mulgnndir  13818  issubg  13840  subggrp  13844  issubg2m  13856  eqgfval  13889  eqgen  13894  quselbasg  13897  quseccl0g  13898  isghm  13910  ghmima  13932  ablressid  14002  gsumfzmptfidmadd  14006  mgpvalg  14017  mgpplusgg  14018  mgptopng  14023  mgpress  14025  rngressid  14048  issrg  14059  ringidss  14123  ring1  14153  ringressid  14157  opprvalg  14163  opprmulfvalg  14164  rdivmuldivd  14239  isnzr2  14279  issubrg  14316  subrgring  14319  rrgval  14357  islmod  14387  scaffvalg  14402  scafvalg  14403  lsssetm  14452  islssm  14453  islssmg  14454  lss1d  14479  lspfval  14484  lspval  14486  lspcl  14487  ellspsn  14513  rnglidlmmgm  14592  rnglidlmsgrp  14593  2idlval  14598  2idlvalg  14599  qusrhm  14624  zlmval  14723  zlmvscag  14729  znval  14732  znle  14733  znbaslemnn  14735  znbas  14740  znzrhval  14743  znleval  14749  psrval  14762  psrbasg  14775  psrelbas  14776  psrplusgg  14779  mplvalcoe  14791  mplbascoe  14792  mplplusgg  14804  topopn  14819  topcld  14920  uncld  14924  iuncld  14926  unicld  14927  tgrest  14980  restin  14987  cnco  15032  cnrest  15046  cnptoprest2  15051  lmss  15057  txbasval  15078  txcn  15086  cnmpt12f  15097  hmeoco  15127  idhmeo  15128  blres  15245  metrest  15317  qtopbasss  15332  tgqioo  15366  divcnap  15376  fsumcncntop  15378  cncfmet  15403  sub1cncf  15413  sub2cncf  15414  cdivcncfap  15415  cnrehmeocntop  15421  cnplimcim  15478  limccnpcntop  15486  limccnp2lem  15487  limccnp2cntop  15488  dvfvalap  15492  dvidsslem  15504  dvmptfsum  15536  plyid  15557  fsumdvdsmul  15805  gausslemma2dlem0b  15869  gausslemma2dlem0d  15871  gausslemma2dlem0h  15875  gausslemma2dlem5a  15884  gausslemma2dlem5  15885  gausslemma2dlem6  15886  lgseisenlem1  15889  lgseisenlem2  15890  lgseisenlem3  15891  lgseisenlem4  15892  2lgslem2  15911  2sqlem8  15942  struct2slots2dom  15979  structiedg0val  15981  edgstruct  16005  uhgrunop  16028  incistruhgr  16031  upgrunop  16068  umgrunop  16070  usgredg2v  16165  usgriedgdomord  16166  uspgredgdomord  16170  subgruhgredgdm  16211  uhgrspansubgrlem  16217  uhgrspanop  16223  upgrspanop  16224  umgrspanop  16225  usgrspanop  16226  vtxdgfval  16229  wksfval  16263  wlk1walkdom  16300  clwwlkg  16334  trlsegvdeglem3  16403  trlsegvdeglem5  16405  eupthvdres  16416  eupth2lem3fi  16417  eupth2lembfi  16418  bj-snexg  16628  trilpolemcl  16769  gsumgfsumlem  16812  gfsumcl  16816