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  4161  rabexd  4178  otexg  4263  tpexg  4479  dmresexg  4969  f1oabexg  5516  funfvex  5575  riotaexg  5881  riotaprop  5901  fnovex  5955  ovexg  5956  fovcdm  6066  fnovrn  6071  cofunexg  6166  cofunex2g  6167  abrexex2g  6177  xpexgALT  6190  mpofvex  6263  tfrex  6426  frec0g  6455  freccllem  6460  ecexg  6596  qsexg  6650  pmex  6712  elixpsn  6794  diffifi  6955  unfidisj  6983  prfidisj  6988  tpfidisj  6990  tpfidceq  6991  ssfirab  6997  ssfidc  6998  fnfi  7002  funrnfi  7008  iunfidisj  7012  infclti  7089  supex2g  7099  infex2g  7100  djuex  7109  ctssdccl  7177  addvalex  7911  negcl  8226  intqfrac2  10411  intfracq  10412  frec2uzzd  10492  frecuzrdgrrn  10500  iseqf1olemqpcl  10601  seq3f1olemqsum  10605  seqf1oglem1  10611  seqf1oglem2  10612  bcval5  10855  xrmaxiflemval  11415  climmpt  11465  reccn2ap  11478  zsumdc  11549  fsumzcl2  11570  fsump1i  11598  fsumabs  11630  hash2iun1dif1  11645  mertenslemi1  11700  fprodcllemf  11778  bitsfzolem  12118  nninfctlemfo  12207  algrf  12213  algcvg  12216  algcvga  12219  algfx  12220  eucalgcvga  12226  eucalg  12227  crth  12392  phimullem  12393  eulerthlemth  12400  prmdiv  12403  pythagtriplem11  12443  pythagtriplem13  12445  pcprecl  12458  infpnlem1  12528  infpnlem2  12529  4sqlem5  12551  mul4sqlem  12562  4sqlemafi  12564  4sqlem13m  12572  4sqlem14  12573  4sqlem17  12576  4sqlem18  12577  ennnfonelemj0  12618  ennnfonelemom  12625  ressbasid  12748  ressval3d  12750  1strbas  12795  2strbasg  12797  2stropg  12798  restid  12921  topnvalg  12922  topnidg  12923  imasival  12949  imasmulr  12952  imasaddfn  12960  imasaddval  12961  imasaddf  12962  imasmulfn  12963  imasmulval  12964  imasmulf  12965  qusval  12966  qusaddval  12978  qusaddf  12979  qusmulval  12980  qusmulf  12981  xpsval  12995  plusffvalg  13005  plusfvalg  13006  grpidvalg  13016  igsumvalx  13032  gsumfzval  13034  gsum0g  13039  gsumsplit1r  13041  gsumprval  13042  issubmnd  13083  ress0g  13084  ismhm  13093  0mhm  13118  grpinvfvalg  13174  grpinvval  13175  grpinvfng  13176  grpsubfvalg  13177  grpsubval  13178  grpressid  13193  grplactfval  13233  mulgfvalg  13251  mulgval  13252  mulgfng  13254  mulgnngsum  13257  mulgnnp1  13260  mulgnndir  13281  issubg  13303  subggrp  13307  issubg2m  13319  eqgfval  13352  eqgen  13357  quselbasg  13360  quseccl0g  13361  isghm  13373  ghmima  13395  ablressid  13465  gsumfzmptfidmadd  13469  mgpvalg  13479  mgpplusgg  13480  mgptopng  13485  mgpress  13487  rngressid  13510  issrg  13521  ringidss  13585  ring1  13615  ringressid  13619  opprvalg  13625  opprmulfvalg  13626  rdivmuldivd  13700  isnzr2  13740  issubrg  13777  subrgring  13780  rrgval  13818  islmod  13847  scaffvalg  13862  scafvalg  13863  lsssetm  13912  islssm  13913  islssmg  13914  lss1d  13939  lspfval  13944  lspval  13946  lspcl  13947  ellspsn  13973  rnglidlmmgm  14052  rnglidlmsgrp  14053  2idlval  14058  2idlvalg  14059  qusrhm  14084  zlmval  14183  zlmvscag  14189  znval  14192  znle  14193  znbaslemnn  14195  znbas  14200  znzrhval  14203  znleval  14209  psrval  14220  psrbasg  14227  psrelbas  14228  psrplusgg  14230  topopn  14244  topcld  14345  uncld  14349  iuncld  14351  unicld  14352  tgrest  14405  restin  14412  cnco  14457  cnrest  14471  cnptoprest2  14476  lmss  14482  txbasval  14503  txcn  14511  cnmpt12f  14522  hmeoco  14552  idhmeo  14553  blres  14670  metrest  14742  qtopbasss  14757  tgqioo  14791  divcnap  14801  fsumcncntop  14803  cncfmet  14828  sub1cncf  14838  sub2cncf  14839  cdivcncfap  14840  cnrehmeocntop  14846  cnplimcim  14903  limccnpcntop  14911  limccnp2lem  14912  limccnp2cntop  14913  dvfvalap  14917  dvidsslem  14929  dvmptfsum  14961  plyid  14982  fsumdvdsmul  15227  gausslemma2dlem0b  15291  gausslemma2dlem0d  15293  gausslemma2dlem0h  15297  gausslemma2dlem5a  15306  gausslemma2dlem5  15307  gausslemma2dlem6  15308  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  2lgslem2  15333  2sqlem8  15364  bj-snexg  15558  trilpolemcl  15681