Theorem eqeltrid 2283

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eqeltrrid  2284  csbexga  4162  rabexd  4179  otexg  4264  tpexg  4480  dmresexg  4970  f1oabexg  5519  funfvex  5578  riotaexg  5884  riotaprop  5904  fnovex  5958  ovexg  5959  fovcdm  6070  fnovrn  6075  cofunexg  6175  cofunex2g  6176  abrexex2g  6186  xpexgALT  6199  mpofvex  6272  tfrex  6435  frec0g  6464  freccllem  6469  ecexg  6605  qsexg  6659  pmex  6721  elixpsn  6803  diffifi  6964  unfidisj  6992  prfidisj  6997  tpfidisj  6999  tpfidceq  7000  ssfirab  7006  ssfidc  7007  fnfi  7011  funrnfi  7017  iunfidisj  7021  infclti  7098  supex2g  7108  infex2g  7109  djuex  7118  ctssdccl  7186  addvalex  7930  negcl  8245  intqfrac2  10430  intfracq  10431  frec2uzzd  10511  frecuzrdgrrn  10519  iseqf1olemqpcl  10620  seq3f1olemqsum  10624  seqf1oglem1  10630  seqf1oglem2  10631  bcval5  10874  xrmaxiflemval  11434  climmpt  11484  reccn2ap  11497  zsumdc  11568  fsumzcl2  11589  fsump1i  11617  fsumabs  11649  hash2iun1dif1  11664  mertenslemi1  11719  fprodcllemf  11797  bitsfzolem  12138  nninfctlemfo  12234  algrf  12240  algcvg  12243  algcvga  12246  algfx  12247  eucalgcvga  12253  eucalg  12254  crth  12419  phimullem  12420  eulerthlemth  12427  prmdiv  12430  pythagtriplem11  12470  pythagtriplem13  12472  pcprecl  12485  infpnlem1  12555  infpnlem2  12556  4sqlem5  12578  mul4sqlem  12589  4sqlemafi  12591  4sqlem13m  12599  4sqlem14  12600  4sqlem17  12603  4sqlem18  12604  ennnfonelemj0  12645  ennnfonelemom  12652  ressbasid  12775  ressval3d  12777  1strbas  12822  2strbasg  12824  2stropg  12825  restid  12954  topnvalg  12955  topnidg  12956  prdsval  12977  prdsplusg  12981  prdsmulr  12982  pwsval  12995  pwselbasb  12997  pwssnf1o  13002  imasival  13010  imasmulr  13013  imasaddfn  13021  imasaddval  13022  imasaddf  13023  imasmulfn  13024  imasmulval  13025  imasmulf  13026  qusval  13027  qusaddval  13039  qusaddf  13040  qusmulval  13041  qusmulf  13042  xpsval  13056  plusffvalg  13066  plusfvalg  13067  grpidvalg  13077  igsumvalx  13093  gsumfzval  13095  gsum0g  13100  gsumsplit1r  13102  gsumprval  13103  prdssgrpd  13119  issubmnd  13146  ress0g  13147  ismhm  13165  0mhm  13190  grpinvfvalg  13246  grpinvval  13247  grpinvfng  13248  grpsubfvalg  13249  grpsubval  13250  grpressid  13265  grplactfval  13305  prdsinvlem  13312  mulgfvalg  13329  mulgval  13330  mulgfng  13332  mulgnngsum  13335  mulgnnp1  13338  mulgnndir  13359  issubg  13381  subggrp  13385  issubg2m  13397  eqgfval  13430  eqgen  13435  quselbasg  13438  quseccl0g  13439  isghm  13451  ghmima  13473  ablressid  13543  gsumfzmptfidmadd  13547  mgpvalg  13557  mgpplusgg  13558  mgptopng  13563  mgpress  13565  rngressid  13588  issrg  13599  ringidss  13663  ring1  13693  ringressid  13697  opprvalg  13703  opprmulfvalg  13704  rdivmuldivd  13778  isnzr2  13818  issubrg  13855  subrgring  13858  rrgval  13896  islmod  13925  scaffvalg  13940  scafvalg  13941  lsssetm  13990  islssm  13991  islssmg  13992  lss1d  14017  lspfval  14022  lspval  14024  lspcl  14025  ellspsn  14051  rnglidlmmgm  14130  rnglidlmsgrp  14131  2idlval  14136  2idlvalg  14137  qusrhm  14162  zlmval  14261  zlmvscag  14267  znval  14270  znle  14271  znbaslemnn  14273  znbas  14278  znzrhval  14281  znleval  14287  psrval  14300  psrbasg  14308  psrelbas  14309  psrplusgg  14312  mplvalcoe  14324  mplbascoe  14325  mplplusgg  14337  topopn  14352  topcld  14453  uncld  14457  iuncld  14459  unicld  14460  tgrest  14513  restin  14520  cnco  14565  cnrest  14579  cnptoprest2  14584  lmss  14590  txbasval  14611  txcn  14619  cnmpt12f  14630  hmeoco  14660  idhmeo  14661  blres  14778  metrest  14850  qtopbasss  14865  tgqioo  14899  divcnap  14909  fsumcncntop  14911  cncfmet  14936  sub1cncf  14946  sub2cncf  14947  cdivcncfap  14948  cnrehmeocntop  14954  cnplimcim  15011  limccnpcntop  15019  limccnp2lem  15020  limccnp2cntop  15021  dvfvalap  15025  dvidsslem  15037  dvmptfsum  15069  plyid  15090  fsumdvdsmul  15335  gausslemma2dlem0b  15399  gausslemma2dlem0d  15401  gausslemma2dlem0h  15405  gausslemma2dlem5a  15414  gausslemma2dlem5  15415  gausslemma2dlem6  15416  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem3  15421  lgseisenlem4  15422  2lgslem2  15441  2sqlem8  15472  bj-snexg  15666  trilpolemcl  15794