Theorem eqeltrid 2325

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eqeltrrid  2326  csbexga  4263  rabexd  4283  otexg  4372  tpexg  4592  dmresexg  5088  f1oabexg  5654  funfvex  5715  elfvfvex  5733  riotaexg  6045  riotaeqimp  6066  riotaprop  6067  fnovex  6121  ovexg  6122  elovimad  6132  fovcdm  6235  fnovrn  6240  cofunexg  6342  cofunex2g  6343  abrexex2g  6353  xpexgALT  6370  mpofvex  6445  mptsuppdifd  6499  tfrex  6643  frec0g  6672  freccllem  6677  ecexg  6815  qsexg  6869  pmex  6931  elixpsn  7021  diffifi  7202  unfidisj  7233  prfidisj  7238  tpfidisj  7240  tpfidceq  7241  ssfirab  7248  ssfidc  7249  fnfi  7254  funrnfi  7260  iunfidisj  7264  infclti  7369  supex2g  7379  infex2g  7380  djuex  7389  ctssdccl  7457  addvalex  8217  negcl  8533  intqfrac2  10777  intfracq  10778  frec2uzzd  10858  frecuzrdgrrn  10866  iseqf1olemqpcl  10967  seq3f1olemqsum  10971  seqf1oglem1  10977  seqf1oglem2  10978  bcval5  11223  hashf1lem2  11308  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccatin12  11527  pfxccat3  11528  pfxccatpfx2  11531  pfxccat3a  11532  swrdccat3blem  11533  swrdccat3b  11534  cats1cld  11557  xrmaxiflemval  12041  climmpt  12091  reccn2ap  12104  zsumdc  12176  fsumzcl2  12197  fsump1i  12225  fsumabs  12257  hash2iun1dif1  12272  mertenslemi1  12327  fprodcllemf  12405  bitsfzolem  12746  nninfctlemfo  12842  algrf  12848  algcvg  12851  algcvga  12854  algfx  12855  eucalgcvga  12861  eucalg  12862  crth  13031  phimullem  13032  eulerthlemth  13039  prmdiv  13042  pythagtriplem11  13082  pythagtriplem13  13084  pcprecl  13097  infpnlem1  13167  infpnlem2  13168  4sqlem5  13190  mul4sqlem  13201  4sqlemafi  13203  4sqlem13m  13211  4sqlem14  13212  4sqlem17  13215  4sqlem18  13216  ennnfonelemj0  13350  ennnfonelemom  13357  ressbasid  13483  ressval3d  13485  1strbas  13530  2strbasg  13533  2stropg  13534  restid  13663  topnvalg  13664  topnidg  13665  imasival  13686  imasmulr  13689  imasaddfn  13697  imasaddval  13698  imasaddf  13699  imasmulfn  13700  imasmulval  13701  imasmulf  13702  qusval  13703  qusaddval  13715  qusaddf  13716  qusmulval  13717  qusmulf  13718  plusffvalg  13741  plusfvalg  13742  grpidvalg  13752  gzsumvalx  13768  gzsumfzval  13770  gzsum0  13772  gzsumsplit1r  13774  issubmnd  13814  ress0g  13815  ismhm  13827  0mhm  13852  grpinvfvalg  13906  grpinvval  13907  grpinvfng  13908  grpsubfvalg  13909  grpsubval  13910  grpressid  13925  grplactfval  13965  mulgfvalg  13983  mulgval  13984  mulgfng  13986  mulgnngzsum  13989  mulgnnp1  13992  mulgnndir  14013  issubg  14035  subggrp  14039  issubg2m  14051  eqgfval  14084  eqgen  14089  quselbasg  14092  quseccl0g  14093  isghm  14105  ghmima  14127  cntzex  14150  cntrval  14151  cntzfval  14152  cntzval  14153  cntrnsg  14176  ablressid  14229  gzsumshift  14239  gsumclfi  14249  gsumsubmclfi  14253  gsum2dfilem1  14271  gsum2dfilem2  14272  gsum2d2fi  14274  prdsval  14280  prdsplusg  14284  prdsmulr  14285  prdssgrpd  14298  prdsinvlem  14303  xpsval  14308  pwsval  14311  pwselbasb  14313  pwssnf1o  14318  mgpvalg  14327  mgpplusgg  14328  mgptopng  14335  mgpress  14337  rngressid  14360  issrg  14376  ringidss  14441  ring1  14471  ringressid  14477  opprvalg  14483  opprmulfvalg  14484  rdivmuldivd  14560  isnzr2  14600  issubrg  14638  subrgring  14641  rrgval  14679  islmod  14736  scaffvalg  14752  scafvalg  14753  lsssetm  14802  islssm  14803  islssmg  14804  lss1d  14829  lspfval  14834  lspval  14836  lspcl  14837  ellspsn  14863  rnglidlmmgm  14942  rnglidlmsgrp  14943  2idlval  14948  2idlvalg  14949  qusrhm  14974  zlmval  15071  zlmvscag  15077  znval  15080  znle  15081  znbaslemnn  15083  znbas  15088  znzrhval  15091  znleval  15097  aspval  15124  asclfval  15130  psrval  15159  gsumbagdiagfi  15176  psrass1filem  15177  psrbasg  15178  psrelbas  15179  psrplusgg  15182  psrmulrg  15186  psrlidmfi  15199  psrridmfi  15200  mplvalcoe  15206  mplbascoe  15207  mplplusgg  15219  topopn  15234  topcld  15335  uncld  15339  iuncld  15341  unicld  15342  tgrest  15395  restin  15402  cnco  15447  cnrest  15461  cnptoprest2  15466  lmss  15472  txbasval  15493  txcn  15501  cnmpt12f  15512  hmeoco  15542  idhmeo  15543  blres  15660  metrest  15732  qtopbasss  15747  tgqioo  15781  divcnap  15791  fsumcncntop  15793  cncfmet  15818  sub1cncf  15828  sub2cncf  15829  cdivcncfap  15830  cnrehmeocntop  15836  cnplimcim  15893  limccnpcntop  15901  limccnp2lem  15902  limccnp2cntop  15903  dvfvalap  15907  dvidsslem  15919  dvmptfsum  15951  plyid  15972  logfac  16126  fsumdvdsmul  16285  bposlem3  16313  bposlem5  16315  bposlem6  16316  gausslemma2dlem0b  16374  gausslemma2dlem0d  16376  gausslemma2dlem0h  16380  gausslemma2dlem5a  16389  gausslemma2dlem5  16390  gausslemma2dlem6  16391  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem3  16396  lgseisenlem4  16397  2lgslem2  16416  2sqlem8  16447  struct2slots2dom  16484  structiedg0val  16486  edgstruct  16510  uhgrunop  16533  incistruhgr  16536  upgrunop  16573  umgrunop  16575  usgredg2v  16670  usgriedgdomord  16671  uspgredgdomord  16675  subgruhgredgdm  16716  uhgrspansubgrlem  16722  uhgrspanop  16728  upgrspanop  16729  umgrspanop  16730  usgrspanop  16731  vtxdgfval  16734  wksfval  16768  wlk1walkdom  16805  clwwlkg  16839  trlsegvdeglem3  16908  trlsegvdeglem5  16910  eupthvdres  16921  eupth2lem3fi  16922  eupth2lembfi  16923  bj-snexg  17143  trilpolemcl  17293