Theorem eqeltrid 2291

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

Syntax hints:   → wi 4   = wceq 1372   ∈ wcel 2175

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200

This theorem is referenced by:  eqeltrrid  2292  csbexga  4171  rabexd  4188  otexg  4273  tpexg  4489  dmresexg  4979  f1oabexg  5528  funfvex  5587  riotaexg  5893  riotaprop  5913  fnovex  5967  ovexg  5968  fovcdm  6079  fnovrn  6084  cofunexg  6184  cofunex2g  6185  abrexex2g  6195  xpexgALT  6208  mpofvex  6281  tfrex  6444  frec0g  6473  freccllem  6478  ecexg  6614  qsexg  6668  pmex  6730  elixpsn  6812  diffifi  6973  unfidisj  7001  prfidisj  7006  tpfidisj  7008  tpfidceq  7009  ssfirab  7015  ssfidc  7016  fnfi  7020  funrnfi  7026  iunfidisj  7030  infclti  7107  supex2g  7117  infex2g  7118  djuex  7127  ctssdccl  7195  addvalex  7939  negcl  8254  intqfrac2  10445  intfracq  10446  frec2uzzd  10526  frecuzrdgrrn  10534  iseqf1olemqpcl  10635  seq3f1olemqsum  10639  seqf1oglem1  10645  seqf1oglem2  10646  bcval5  10889  xrmaxiflemval  11480  climmpt  11530  reccn2ap  11543  zsumdc  11614  fsumzcl2  11635  fsump1i  11663  fsumabs  11695  hash2iun1dif1  11710  mertenslemi1  11765  fprodcllemf  11843  bitsfzolem  12184  nninfctlemfo  12280  algrf  12286  algcvg  12289  algcvga  12292  algfx  12293  eucalgcvga  12299  eucalg  12300  crth  12465  phimullem  12466  eulerthlemth  12473  prmdiv  12476  pythagtriplem11  12516  pythagtriplem13  12518  pcprecl  12531  infpnlem1  12601  infpnlem2  12602  4sqlem5  12624  mul4sqlem  12635  4sqlemafi  12637  4sqlem13m  12645  4sqlem14  12646  4sqlem17  12649  4sqlem18  12650  ennnfonelemj0  12691  ennnfonelemom  12698  ressbasid  12821  ressval3d  12823  1strbas  12868  2strbasg  12870  2stropg  12871  restid  13000  topnvalg  13001  topnidg  13002  prdsval  13023  prdsplusg  13027  prdsmulr  13028  pwsval  13041  pwselbasb  13043  pwssnf1o  13048  imasival  13056  imasmulr  13059  imasaddfn  13067  imasaddval  13068  imasaddf  13069  imasmulfn  13070  imasmulval  13071  imasmulf  13072  qusval  13073  qusaddval  13085  qusaddf  13086  qusmulval  13087  qusmulf  13088  xpsval  13102  plusffvalg  13112  plusfvalg  13113  grpidvalg  13123  igsumvalx  13139  gsumfzval  13141  gsum0g  13146  gsumsplit1r  13148  gsumprval  13149  prdssgrpd  13165  issubmnd  13192  ress0g  13193  ismhm  13211  0mhm  13236  grpinvfvalg  13292  grpinvval  13293  grpinvfng  13294  grpsubfvalg  13295  grpsubval  13296  grpressid  13311  grplactfval  13351  prdsinvlem  13358  mulgfvalg  13375  mulgval  13376  mulgfng  13378  mulgnngsum  13381  mulgnnp1  13384  mulgnndir  13405  issubg  13427  subggrp  13431  issubg2m  13443  eqgfval  13476  eqgen  13481  quselbasg  13484  quseccl0g  13485  isghm  13497  ghmima  13519  ablressid  13589  gsumfzmptfidmadd  13593  mgpvalg  13603  mgpplusgg  13604  mgptopng  13609  mgpress  13611  rngressid  13634  issrg  13645  ringidss  13709  ring1  13739  ringressid  13743  opprvalg  13749  opprmulfvalg  13750  rdivmuldivd  13824  isnzr2  13864  issubrg  13901  subrgring  13904  rrgval  13942  islmod  13971  scaffvalg  13986  scafvalg  13987  lsssetm  14036  islssm  14037  islssmg  14038  lss1d  14063  lspfval  14068  lspval  14070  lspcl  14071  ellspsn  14097  rnglidlmmgm  14176  rnglidlmsgrp  14177  2idlval  14182  2idlvalg  14183  qusrhm  14208  zlmval  14307  zlmvscag  14313  znval  14316  znle  14317  znbaslemnn  14319  znbas  14324  znzrhval  14327  znleval  14333  psrval  14346  psrbasg  14354  psrelbas  14355  psrplusgg  14358  mplvalcoe  14370  mplbascoe  14371  mplplusgg  14383  topopn  14398  topcld  14499  uncld  14503  iuncld  14505  unicld  14506  tgrest  14559  restin  14566  cnco  14611  cnrest  14625  cnptoprest2  14630  lmss  14636  txbasval  14657  txcn  14665  cnmpt12f  14676  hmeoco  14706  idhmeo  14707  blres  14824  metrest  14896  qtopbasss  14911  tgqioo  14945  divcnap  14955  fsumcncntop  14957  cncfmet  14982  sub1cncf  14992  sub2cncf  14993  cdivcncfap  14994  cnrehmeocntop  15000  cnplimcim  15057  limccnpcntop  15065  limccnp2lem  15066  limccnp2cntop  15067  dvfvalap  15071  dvidsslem  15083  dvmptfsum  15115  plyid  15136  fsumdvdsmul  15381  gausslemma2dlem0b  15445  gausslemma2dlem0d  15447  gausslemma2dlem0h  15451  gausslemma2dlem5a  15460  gausslemma2dlem5  15461  gausslemma2dlem6  15462  lgseisenlem1  15465  lgseisenlem2  15466  lgseisenlem3  15467  lgseisenlem4  15468  2lgslem2  15487  2sqlem8  15518  bj-snexg  15712  trilpolemcl  15840