Theorem eqeltrid 2316

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eqeltrrid  2317  csbexga  4211  rabexd  4228  otexg  4315  tpexg  4534  dmresexg  5027  f1oabexg  5583  funfvex  5643  elfvex  5660  riotaexg  5957  riotaeqimp  5978  riotaprop  5979  fnovex  6033  ovexg  6034  elovimad  6044  fovcdm  6147  fnovrn  6152  cofunexg  6252  cofunex2g  6253  abrexex2g  6263  xpexgALT  6276  mpofvex  6349  tfrex  6512  frec0g  6541  freccllem  6546  ecexg  6682  qsexg  6736  pmex  6798  elixpsn  6880  diffifi  7052  unfidisj  7080  prfidisj  7085  tpfidisj  7087  tpfidceq  7088  ssfirab  7094  ssfidc  7095  fnfi  7099  funrnfi  7105  iunfidisj  7109  infclti  7186  supex2g  7196  infex2g  7197  djuex  7206  ctssdccl  7274  addvalex  8027  negcl  8342  intqfrac2  10536  intfracq  10537  frec2uzzd  10617  frecuzrdgrrn  10625  iseqf1olemqpcl  10726  seq3f1olemqsum  10730  seqf1oglem1  10736  seqf1oglem2  10737  bcval5  10980  swrdccatin2  11256  pfxccatin12lem2  11258  pfxccatin12  11260  pfxccat3  11261  pfxccatpfx2  11264  pfxccat3a  11265  swrdccat3blem  11266  swrdccat3b  11267  cats1cld  11290  xrmaxiflemval  11756  climmpt  11806  reccn2ap  11819  zsumdc  11890  fsumzcl2  11911  fsump1i  11939  fsumabs  11971  hash2iun1dif1  11986  mertenslemi1  12041  fprodcllemf  12119  bitsfzolem  12460  nninfctlemfo  12556  algrf  12562  algcvg  12565  algcvga  12568  algfx  12569  eucalgcvga  12575  eucalg  12576  crth  12741  phimullem  12742  eulerthlemth  12749  prmdiv  12752  pythagtriplem11  12792  pythagtriplem13  12794  pcprecl  12807  infpnlem1  12877  infpnlem2  12878  4sqlem5  12900  mul4sqlem  12911  4sqlemafi  12913  4sqlem13m  12921  4sqlem14  12922  4sqlem17  12925  4sqlem18  12926  ennnfonelemj0  12967  ennnfonelemom  12974  ressbasid  13098  ressval3d  13100  1strbas  13145  2strbasg  13148  2stropg  13149  restid  13278  topnvalg  13279  topnidg  13280  prdsval  13301  prdsplusg  13305  prdsmulr  13306  pwsval  13319  pwselbasb  13321  pwssnf1o  13326  imasival  13334  imasmulr  13337  imasaddfn  13345  imasaddval  13346  imasaddf  13347  imasmulfn  13348  imasmulval  13349  imasmulf  13350  qusval  13351  qusaddval  13363  qusaddf  13364  qusmulval  13365  qusmulf  13366  xpsval  13380  plusffvalg  13390  plusfvalg  13391  grpidvalg  13401  igsumvalx  13417  gsumfzval  13419  gsum0g  13424  gsumsplit1r  13426  gsumprval  13427  prdssgrpd  13443  issubmnd  13470  ress0g  13471  ismhm  13489  0mhm  13514  grpinvfvalg  13570  grpinvval  13571  grpinvfng  13572  grpsubfvalg  13573  grpsubval  13574  grpressid  13589  grplactfval  13629  prdsinvlem  13636  mulgfvalg  13653  mulgval  13654  mulgfng  13656  mulgnngsum  13659  mulgnnp1  13662  mulgnndir  13683  issubg  13705  subggrp  13709  issubg2m  13721  eqgfval  13754  eqgen  13759  quselbasg  13762  quseccl0g  13763  isghm  13775  ghmima  13797  ablressid  13867  gsumfzmptfidmadd  13871  mgpvalg  13881  mgpplusgg  13882  mgptopng  13887  mgpress  13889  rngressid  13912  issrg  13923  ringidss  13987  ring1  14017  ringressid  14021  opprvalg  14027  opprmulfvalg  14028  rdivmuldivd  14102  isnzr2  14142  issubrg  14179  subrgring  14182  rrgval  14220  islmod  14249  scaffvalg  14264  scafvalg  14265  lsssetm  14314  islssm  14315  islssmg  14316  lss1d  14341  lspfval  14346  lspval  14348  lspcl  14349  ellspsn  14375  rnglidlmmgm  14454  rnglidlmsgrp  14455  2idlval  14460  2idlvalg  14461  qusrhm  14486  zlmval  14585  zlmvscag  14591  znval  14594  znle  14595  znbaslemnn  14597  znbas  14602  znzrhval  14605  znleval  14611  psrval  14624  psrbasg  14632  psrelbas  14633  psrplusgg  14636  mplvalcoe  14648  mplbascoe  14649  mplplusgg  14661  topopn  14676  topcld  14777  uncld  14781  iuncld  14783  unicld  14784  tgrest  14837  restin  14844  cnco  14889  cnrest  14903  cnptoprest2  14908  lmss  14914  txbasval  14935  txcn  14943  cnmpt12f  14954  hmeoco  14984  idhmeo  14985  blres  15102  metrest  15174  qtopbasss  15189  tgqioo  15223  divcnap  15233  fsumcncntop  15235  cncfmet  15260  sub1cncf  15270  sub2cncf  15271  cdivcncfap  15272  cnrehmeocntop  15278  cnplimcim  15335  limccnpcntop  15343  limccnp2lem  15344  limccnp2cntop  15345  dvfvalap  15349  dvidsslem  15361  dvmptfsum  15393  plyid  15414  fsumdvdsmul  15659  gausslemma2dlem0b  15723  gausslemma2dlem0d  15725  gausslemma2dlem0h  15729  gausslemma2dlem5a  15738  gausslemma2dlem5  15739  gausslemma2dlem6  15740  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem3  15745  lgseisenlem4  15746  2lgslem2  15765  2sqlem8  15796  struct2slots2dom  15833  structiedg0val  15835  edgstruct  15858  uhgrunop  15881  incistruhgr  15884  upgrunop  15919  umgrunop  15921  usgredg2v  16016  usgriedgdomord  16017  uspgredgdomord  16021  wksfval  16028  bj-snexg  16233  trilpolemcl  16364