Theorem eqeltrid 2280

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

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

This theorem is referenced by:  eqeltrrid  2281  csbexga  4157  rabexd  4174  otexg  4259  tpexg  4475  dmresexg  4965  f1oabexg  5512  funfvex  5571  riotaexg  5877  riotaprop  5897  fnovex  5951  ovexg  5952  fovcdm  6061  fnovrn  6066  cofunexg  6161  cofunex2g  6162  abrexex2g  6172  xpexgALT  6185  mpofvex  6256  tfrex  6421  frec0g  6450  freccllem  6455  ecexg  6591  qsexg  6645  pmex  6707  elixpsn  6789  diffifi  6950  unfidisj  6978  prfidisj  6983  tpfidisj  6984  ssfirab  6990  ssfidc  6991  fnfi  6995  funrnfi  7001  iunfidisj  7005  infclti  7082  supex2g  7092  infex2g  7093  djuex  7102  ctssdccl  7170  addvalex  7904  negcl  8219  intqfrac2  10390  intfracq  10391  frec2uzzd  10471  frecuzrdgrrn  10479  iseqf1olemqpcl  10580  seq3f1olemqsum  10584  seqf1oglem1  10590  seqf1oglem2  10591  bcval5  10834  xrmaxiflemval  11393  climmpt  11443  reccn2ap  11456  zsumdc  11527  fsumzcl2  11548  fsump1i  11576  fsumabs  11608  hash2iun1dif1  11623  mertenslemi1  11678  fprodcllemf  11756  nninfctlemfo  12177  algrf  12183  algcvg  12186  algcvga  12189  algfx  12190  eucalgcvga  12196  eucalg  12197  crth  12362  phimullem  12363  eulerthlemth  12370  prmdiv  12373  pythagtriplem11  12412  pythagtriplem13  12414  pcprecl  12427  infpnlem1  12497  infpnlem2  12498  4sqlem5  12520  mul4sqlem  12531  4sqlemafi  12533  4sqlem13m  12541  4sqlem14  12542  4sqlem17  12545  4sqlem18  12546  ennnfonelemj0  12558  ennnfonelemom  12565  ressbasid  12688  ressval3d  12690  1strbas  12735  2strbasg  12737  2stropg  12738  restid  12861  topnvalg  12862  topnidg  12863  imasival  12889  imasmulr  12892  imasaddfn  12900  imasaddval  12901  imasaddf  12902  imasmulfn  12903  imasmulval  12904  imasmulf  12905  qusval  12906  qusaddval  12918  qusaddf  12919  qusmulval  12920  qusmulf  12921  xpsval  12935  plusffvalg  12945  plusfvalg  12946  grpidvalg  12956  igsumvalx  12972  gsumfzval  12974  gsum0g  12979  gsumsplit1r  12981  gsumprval  12982  issubmnd  13023  ress0g  13024  ismhm  13033  0mhm  13058  grpinvfvalg  13114  grpinvval  13115  grpinvfng  13116  grpsubfvalg  13117  grpsubval  13118  grpressid  13133  grplactfval  13173  mulgfvalg  13191  mulgval  13192  mulgfng  13194  mulgnngsum  13197  mulgnnp1  13200  mulgnndir  13221  issubg  13243  subggrp  13247  issubg2m  13259  eqgfval  13292  eqgen  13297  quselbasg  13300  quseccl0g  13301  isghm  13313  ghmima  13335  ablressid  13405  gsumfzmptfidmadd  13409  mgpvalg  13419  mgpplusgg  13420  mgptopng  13425  mgpress  13427  rngressid  13450  issrg  13461  ringidss  13525  ring1  13555  ringressid  13559  opprvalg  13565  opprmulfvalg  13566  rdivmuldivd  13640  isnzr2  13680  issubrg  13717  subrgring  13720  rrgval  13758  islmod  13787  scaffvalg  13802  scafvalg  13803  lsssetm  13852  islssm  13853  islssmg  13854  lss1d  13879  lspfval  13884  lspval  13886  lspcl  13887  ellspsn  13913  rnglidlmmgm  13992  rnglidlmsgrp  13993  2idlval  13998  2idlvalg  13999  qusrhm  14024  zlmval  14115  zlmvscag  14121  znval  14124  znle  14125  znbaslemnn  14127  znbas  14132  znzrhval  14135  znleval  14141  psrval  14152  psrbasg  14159  psrelbas  14160  psrplusgg  14162  topopn  14176  topcld  14277  uncld  14281  iuncld  14283  unicld  14284  tgrest  14337  restin  14344  cnco  14389  cnrest  14403  cnptoprest2  14408  lmss  14414  txbasval  14435  txcn  14443  cnmpt12f  14454  hmeoco  14484  idhmeo  14485  blres  14602  metrest  14674  qtopbasss  14689  tgqioo  14715  divcnap  14723  fsumcncntop  14724  cncfmet  14747  sub1cncf  14756  sub2cncf  14757  cdivcncfap  14758  cnrehmeocntop  14764  cnplimcim  14821  limccnpcntop  14829  limccnp2lem  14830  limccnp2cntop  14831  dvfvalap  14835  plyid  14892  gausslemma2dlem0b  15166  gausslemma2dlem0d  15168  gausslemma2dlem0h  15172  gausslemma2dlem5a  15181  gausslemma2dlem5  15182  gausslemma2dlem6  15183  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  2sqlem8  15210  bj-snexg  15404  trilpolemcl  15527