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  4212  rabexd  4229  otexg  4316  tpexg  4535  dmresexg  5028  f1oabexg  5586  funfvex  5646  elfvfvex  5663  riotaexg  5964  riotaeqimp  5985  riotaprop  5986  fnovex  6040  ovexg  6041  elovimad  6051  fovcdm  6154  fnovrn  6159  cofunexg  6260  cofunex2g  6261  abrexex2g  6271  xpexgALT  6284  mpofvex  6357  tfrex  6520  frec0g  6549  freccllem  6554  ecexg  6692  qsexg  6746  pmex  6808  elixpsn  6890  diffifi  7064  unfidisj  7095  prfidisj  7100  tpfidisj  7102  tpfidceq  7103  ssfirab  7109  ssfidc  7110  fnfi  7114  funrnfi  7120  iunfidisj  7124  infclti  7201  supex2g  7211  infex2g  7212  djuex  7221  ctssdccl  7289  addvalex  8042  negcl  8357  intqfrac2  10553  intfracq  10554  frec2uzzd  10634  frecuzrdgrrn  10642  iseqf1olemqpcl  10743  seq3f1olemqsum  10747  seqf1oglem1  10753  seqf1oglem2  10754  bcval5  10997  swrdccatin2  11276  pfxccatin12lem2  11278  pfxccatin12  11280  pfxccat3  11281  pfxccatpfx2  11284  pfxccat3a  11285  swrdccat3blem  11286  swrdccat3b  11287  cats1cld  11310  xrmaxiflemval  11776  climmpt  11826  reccn2ap  11839  zsumdc  11910  fsumzcl2  11931  fsump1i  11959  fsumabs  11991  hash2iun1dif1  12006  mertenslemi1  12061  fprodcllemf  12139  bitsfzolem  12480  nninfctlemfo  12576  algrf  12582  algcvg  12585  algcvga  12588  algfx  12589  eucalgcvga  12595  eucalg  12596  crth  12761  phimullem  12762  eulerthlemth  12769  prmdiv  12772  pythagtriplem11  12812  pythagtriplem13  12814  pcprecl  12827  infpnlem1  12897  infpnlem2  12898  4sqlem5  12920  mul4sqlem  12931  4sqlemafi  12933  4sqlem13m  12941  4sqlem14  12942  4sqlem17  12945  4sqlem18  12946  ennnfonelemj0  12987  ennnfonelemom  12994  ressbasid  13118  ressval3d  13120  1strbas  13165  2strbasg  13168  2stropg  13169  restid  13298  topnvalg  13299  topnidg  13300  prdsval  13321  prdsplusg  13325  prdsmulr  13326  pwsval  13339  pwselbasb  13341  pwssnf1o  13346  imasival  13354  imasmulr  13357  imasaddfn  13365  imasaddval  13366  imasaddf  13367  imasmulfn  13368  imasmulval  13369  imasmulf  13370  qusval  13371  qusaddval  13383  qusaddf  13384  qusmulval  13385  qusmulf  13386  xpsval  13400  plusffvalg  13410  plusfvalg  13411  grpidvalg  13421  igsumvalx  13437  gsumfzval  13439  gsum0g  13444  gsumsplit1r  13446  gsumprval  13447  prdssgrpd  13463  issubmnd  13490  ress0g  13491  ismhm  13509  0mhm  13534  grpinvfvalg  13590  grpinvval  13591  grpinvfng  13592  grpsubfvalg  13593  grpsubval  13594  grpressid  13609  grplactfval  13649  prdsinvlem  13656  mulgfvalg  13673  mulgval  13674  mulgfng  13676  mulgnngsum  13679  mulgnnp1  13682  mulgnndir  13703  issubg  13725  subggrp  13729  issubg2m  13741  eqgfval  13774  eqgen  13779  quselbasg  13782  quseccl0g  13783  isghm  13795  ghmima  13817  ablressid  13887  gsumfzmptfidmadd  13891  mgpvalg  13901  mgpplusgg  13902  mgptopng  13907  mgpress  13909  rngressid  13932  issrg  13943  ringidss  14007  ring1  14037  ringressid  14041  opprvalg  14047  opprmulfvalg  14048  rdivmuldivd  14123  isnzr2  14163  issubrg  14200  subrgring  14203  rrgval  14241  islmod  14270  scaffvalg  14285  scafvalg  14286  lsssetm  14335  islssm  14336  islssmg  14337  lss1d  14362  lspfval  14367  lspval  14369  lspcl  14370  ellspsn  14396  rnglidlmmgm  14475  rnglidlmsgrp  14476  2idlval  14481  2idlvalg  14482  qusrhm  14507  zlmval  14606  zlmvscag  14612  znval  14615  znle  14616  znbaslemnn  14618  znbas  14623  znzrhval  14626  znleval  14632  psrval  14645  psrbasg  14653  psrelbas  14654  psrplusgg  14657  mplvalcoe  14669  mplbascoe  14670  mplplusgg  14682  topopn  14697  topcld  14798  uncld  14802  iuncld  14804  unicld  14805  tgrest  14858  restin  14865  cnco  14910  cnrest  14924  cnptoprest2  14929  lmss  14935  txbasval  14956  txcn  14964  cnmpt12f  14975  hmeoco  15005  idhmeo  15006  blres  15123  metrest  15195  qtopbasss  15210  tgqioo  15244  divcnap  15254  fsumcncntop  15256  cncfmet  15281  sub1cncf  15291  sub2cncf  15292  cdivcncfap  15293  cnrehmeocntop  15299  cnplimcim  15356  limccnpcntop  15364  limccnp2lem  15365  limccnp2cntop  15366  dvfvalap  15370  dvidsslem  15382  dvmptfsum  15414  plyid  15435  fsumdvdsmul  15680  gausslemma2dlem0b  15744  gausslemma2dlem0d  15746  gausslemma2dlem0h  15750  gausslemma2dlem5a  15759  gausslemma2dlem5  15760  gausslemma2dlem6  15761  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem3  15766  lgseisenlem4  15767  2lgslem2  15786  2sqlem8  15817  struct2slots2dom  15854  structiedg0val  15856  edgstruct  15879  uhgrunop  15902  incistruhgr  15905  upgrunop  15940  umgrunop  15942  usgredg2v  16037  usgriedgdomord  16038  uspgredgdomord  16042  vtxdgfval  16047  wksfval  16063  wlk1walkdom  16100  clwwlkg  16131  bj-snexg  16330  trilpolemcl  16465