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 1397   ∈ 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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  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  4217  rabexd  4235  otexg  4322  tpexg  4541  dmresexg  5036  f1oabexg  5595  funfvex  5656  elfvfvex  5673  riotaexg  5975  riotaeqimp  5996  riotaprop  5997  fnovex  6051  ovexg  6052  elovimad  6062  fovcdm  6165  fnovrn  6170  cofunexg  6271  cofunex2g  6272  abrexex2g  6282  xpexgALT  6295  mpofvex  6370  tfrex  6534  frec0g  6563  freccllem  6568  ecexg  6706  qsexg  6760  pmex  6822  elixpsn  6904  diffifi  7083  unfidisj  7114  prfidisj  7119  tpfidisj  7121  tpfidceq  7122  ssfirab  7129  ssfidc  7130  fnfi  7135  funrnfi  7141  iunfidisj  7145  infclti  7222  supex2g  7232  infex2g  7233  djuex  7242  ctssdccl  7310  addvalex  8064  negcl  8379  intqfrac2  10582  intfracq  10583  frec2uzzd  10663  frecuzrdgrrn  10671  iseqf1olemqpcl  10772  seq3f1olemqsum  10776  seqf1oglem1  10782  seqf1oglem2  10783  bcval5  11026  swrdccatin2  11311  pfxccatin12lem2  11313  pfxccatin12  11315  pfxccat3  11316  pfxccatpfx2  11319  pfxccat3a  11320  swrdccat3blem  11321  swrdccat3b  11322  cats1cld  11345  xrmaxiflemval  11812  climmpt  11862  reccn2ap  11875  zsumdc  11947  fsumzcl2  11968  fsump1i  11996  fsumabs  12028  hash2iun1dif1  12043  mertenslemi1  12098  fprodcllemf  12176  bitsfzolem  12517  nninfctlemfo  12613  algrf  12619  algcvg  12622  algcvga  12625  algfx  12626  eucalgcvga  12632  eucalg  12633  crth  12798  phimullem  12799  eulerthlemth  12806  prmdiv  12809  pythagtriplem11  12849  pythagtriplem13  12851  pcprecl  12864  infpnlem1  12934  infpnlem2  12935  4sqlem5  12957  mul4sqlem  12968  4sqlemafi  12970  4sqlem13m  12978  4sqlem14  12979  4sqlem17  12982  4sqlem18  12983  ennnfonelemj0  13024  ennnfonelemom  13031  ressbasid  13155  ressval3d  13157  1strbas  13202  2strbasg  13205  2stropg  13206  restid  13335  topnvalg  13336  topnidg  13337  prdsval  13358  prdsplusg  13362  prdsmulr  13363  pwsval  13376  pwselbasb  13378  pwssnf1o  13383  imasival  13391  imasmulr  13394  imasaddfn  13402  imasaddval  13403  imasaddf  13404  imasmulfn  13405  imasmulval  13406  imasmulf  13407  qusval  13408  qusaddval  13420  qusaddf  13421  qusmulval  13422  qusmulf  13423  xpsval  13437  plusffvalg  13447  plusfvalg  13448  grpidvalg  13458  igsumvalx  13474  gsumfzval  13476  gsum0g  13481  gsumsplit1r  13483  gsumprval  13484  prdssgrpd  13500  issubmnd  13527  ress0g  13528  ismhm  13546  0mhm  13571  grpinvfvalg  13627  grpinvval  13628  grpinvfng  13629  grpsubfvalg  13630  grpsubval  13631  grpressid  13646  grplactfval  13686  prdsinvlem  13693  mulgfvalg  13710  mulgval  13711  mulgfng  13713  mulgnngsum  13716  mulgnnp1  13719  mulgnndir  13740  issubg  13762  subggrp  13766  issubg2m  13778  eqgfval  13811  eqgen  13816  quselbasg  13819  quseccl0g  13820  isghm  13832  ghmima  13854  ablressid  13924  gsumfzmptfidmadd  13928  mgpvalg  13939  mgpplusgg  13940  mgptopng  13945  mgpress  13947  rngressid  13970  issrg  13981  ringidss  14045  ring1  14075  ringressid  14079  opprvalg  14085  opprmulfvalg  14086  rdivmuldivd  14161  isnzr2  14201  issubrg  14238  subrgring  14241  rrgval  14279  islmod  14308  scaffvalg  14323  scafvalg  14324  lsssetm  14373  islssm  14374  islssmg  14375  lss1d  14400  lspfval  14405  lspval  14407  lspcl  14408  ellspsn  14434  rnglidlmmgm  14513  rnglidlmsgrp  14514  2idlval  14519  2idlvalg  14520  qusrhm  14545  zlmval  14644  zlmvscag  14650  znval  14653  znle  14654  znbaslemnn  14656  znbas  14661  znzrhval  14664  znleval  14670  psrval  14683  psrbasg  14691  psrelbas  14692  psrplusgg  14695  mplvalcoe  14707  mplbascoe  14708  mplplusgg  14720  topopn  14735  topcld  14836  uncld  14840  iuncld  14842  unicld  14843  tgrest  14896  restin  14903  cnco  14948  cnrest  14962  cnptoprest2  14967  lmss  14973  txbasval  14994  txcn  15002  cnmpt12f  15013  hmeoco  15043  idhmeo  15044  blres  15161  metrest  15233  qtopbasss  15248  tgqioo  15282  divcnap  15292  fsumcncntop  15294  cncfmet  15319  sub1cncf  15329  sub2cncf  15330  cdivcncfap  15331  cnrehmeocntop  15337  cnplimcim  15394  limccnpcntop  15402  limccnp2lem  15403  limccnp2cntop  15404  dvfvalap  15408  dvidsslem  15420  dvmptfsum  15452  plyid  15473  fsumdvdsmul  15718  gausslemma2dlem0b  15782  gausslemma2dlem0d  15784  gausslemma2dlem0h  15788  gausslemma2dlem5a  15797  gausslemma2dlem5  15798  gausslemma2dlem6  15799  lgseisenlem1  15802  lgseisenlem2  15803  lgseisenlem3  15804  lgseisenlem4  15805  2lgslem2  15824  2sqlem8  15855  struct2slots2dom  15892  structiedg0val  15894  edgstruct  15918  uhgrunop  15941  incistruhgr  15944  upgrunop  15981  umgrunop  15983  usgredg2v  16078  usgriedgdomord  16079  uspgredgdomord  16083  subgruhgredgdm  16124  uhgrspansubgrlem  16130  uhgrspanop  16136  upgrspanop  16137  umgrspanop  16138  usgrspanop  16139  vtxdgfval  16142  wksfval  16176  wlk1walkdom  16213  clwwlkg  16247  trlsegvdeglem3  16316  trlsegvdeglem5  16318  eupthvdres  16329  eupth2lem3fi  16330  eupth2lembfi  16331  bj-snexg  16524  trilpolemcl  16658  gsumgfsumlem  16700  gfsumcl  16704