Theorem eqeltrid 2321

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 2311	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1398   ∈ 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:  eqeltrrid  2322  csbexga  4243  rabexd  4262  otexg  4351  tpexg  4570  dmresexg  5066  f1oabexg  5631  funfvex  5692  elfvfvex  5709  riotaexg  6015  riotaeqimp  6036  riotaprop  6037  fnovex  6091  ovexg  6092  elovimad  6102  fovcdm  6205  fnovrn  6210  cofunexg  6311  cofunex2g  6312  abrexex2g  6322  xpexgALT  6339  mpofvex  6414  mptsuppdifd  6468  tfrex  6612  frec0g  6641  freccllem  6646  ecexg  6784  qsexg  6838  pmex  6900  elixpsn  6983  diffifi  7164  unfidisj  7195  prfidisj  7200  tpfidisj  7202  tpfidceq  7203  ssfirab  7210  ssfidc  7211  fnfi  7216  funrnfi  7222  iunfidisj  7226  infclti  7327  supex2g  7337  infex2g  7338  djuex  7347  ctssdccl  7415  addvalex  8175  negcl  8489  intqfrac2  10705  intfracq  10706  frec2uzzd  10786  frecuzrdgrrn  10794  iseqf1olemqpcl  10895  seq3f1olemqsum  10899  seqf1oglem1  10905  seqf1oglem2  10906  bcval5  11150  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12  11450  pfxccat3  11451  pfxccatpfx2  11454  pfxccat3a  11455  swrdccat3blem  11456  swrdccat3b  11457  cats1cld  11480  xrmaxiflemval  11960  climmpt  12010  reccn2ap  12023  zsumdc  12095  fsumzcl2  12116  fsump1i  12144  fsumabs  12176  hash2iun1dif1  12191  mertenslemi1  12246  fprodcllemf  12324  bitsfzolem  12665  nninfctlemfo  12761  algrf  12767  algcvg  12770  algcvga  12773  algfx  12774  eucalgcvga  12780  eucalg  12781  crth  12946  phimullem  12947  eulerthlemth  12954  prmdiv  12957  pythagtriplem11  12997  pythagtriplem13  12999  pcprecl  13012  infpnlem1  13082  infpnlem2  13083  4sqlem5  13105  mul4sqlem  13116  4sqlemafi  13118  4sqlem13m  13126  4sqlem14  13127  4sqlem17  13130  4sqlem18  13131  ennnfonelemj0  13236  ennnfonelemom  13243  ressbasid  13367  ressval3d  13369  1strbas  13414  2strbasg  13417  2stropg  13418  restid  13547  topnvalg  13548  topnidg  13549  imasival  13570  imasmulr  13573  imasaddfn  13581  imasaddval  13582  imasaddf  13583  imasmulfn  13584  imasmulval  13585  imasmulf  13586  qusval  13587  qusaddval  13599  qusaddf  13600  qusmulval  13601  qusmulf  13602  plusffvalg  13625  plusfvalg  13626  grpidvalg  13636  igsumvalx  13652  gsumfzval  13654  gsum0g  13659  gsumsplit1r  13661  gsumprval  13662  issubmnd  13703  ress0g  13704  ismhm  13716  0mhm  13741  grpinvfvalg  13797  grpinvval  13798  grpinvfng  13799  grpsubfvalg  13800  grpsubval  13801  grpressid  13816  grplactfval  13856  mulgfvalg  13874  mulgval  13875  mulgfng  13877  mulgnngsum  13880  mulgnnp1  13883  mulgnndir  13904  issubg  13926  subggrp  13930  issubg2m  13942  eqgfval  13975  eqgen  13980  quselbasg  13983  quseccl0g  13984  isghm  13996  ghmima  14018  ablressid  14088  gsumfzmptfidmadd  14092  gsumshift  14105  gfsumcl  14110  prdsval  14115  prdsplusg  14119  prdsmulr  14120  prdssgrpd  14133  prdsinvlem  14138  xpsval  14143  pwsval  14146  pwselbasb  14148  pwssnf1o  14153  mgpvalg  14162  mgpplusgg  14163  mgptopng  14168  mgpress  14170  rngressid  14193  issrg  14208  ringidss  14272  ring1  14302  ringressid  14306  opprvalg  14312  opprmulfvalg  14313  rdivmuldivd  14389  isnzr2  14429  issubrg  14467  subrgring  14470  rrgval  14508  islmod  14565  scaffvalg  14580  scafvalg  14581  lsssetm  14630  islssm  14631  islssmg  14632  lss1d  14657  lspfval  14662  lspval  14664  lspcl  14665  ellspsn  14691  rnglidlmmgm  14770  rnglidlmsgrp  14771  2idlval  14776  2idlvalg  14777  qusrhm  14802  zlmval  14901  zlmvscag  14907  znval  14910  znle  14911  znbaslemnn  14913  znbas  14918  znzrhval  14921  znleval  14927  psrval  14940  psrbasg  14955  psrelbas  14956  psrplusgg  14959  mplvalcoe  14971  mplbascoe  14972  mplplusgg  14984  topopn  14999  topcld  15100  uncld  15104  iuncld  15106  unicld  15107  tgrest  15160  restin  15167  cnco  15212  cnrest  15226  cnptoprest2  15231  lmss  15237  txbasval  15258  txcn  15266  cnmpt12f  15277  hmeoco  15307  idhmeo  15308  blres  15425  metrest  15497  qtopbasss  15512  tgqioo  15546  divcnap  15556  fsumcncntop  15558  cncfmet  15583  sub1cncf  15593  sub2cncf  15594  cdivcncfap  15595  cnrehmeocntop  15601  cnplimcim  15658  limccnpcntop  15666  limccnp2lem  15667  limccnp2cntop  15668  dvfvalap  15672  dvidsslem  15684  dvmptfsum  15716  plyid  15737  fsumdvdsmul  15985  gausslemma2dlem0b  16049  gausslemma2dlem0d  16051  gausslemma2dlem0h  16055  gausslemma2dlem5a  16064  gausslemma2dlem5  16065  gausslemma2dlem6  16066  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgseisenlem4  16072  2lgslem2  16091  2sqlem8  16122  struct2slots2dom  16159  structiedg0val  16161  edgstruct  16185  uhgrunop  16208  incistruhgr  16211  upgrunop  16248  umgrunop  16250  usgredg2v  16345  usgriedgdomord  16346  uspgredgdomord  16350  subgruhgredgdm  16391  uhgrspansubgrlem  16397  uhgrspanop  16403  upgrspanop  16404  umgrspanop  16405  usgrspanop  16406  vtxdgfval  16409  wksfval  16443  wlk1walkdom  16480  clwwlkg  16514  trlsegvdeglem3  16583  trlsegvdeglem5  16585  eupthvdres  16596  eupth2lem3fi  16597  eupth2lembfi  16598  bj-snexg  16808  trilpolemcl  16947