Theorem eqeltrid 2293

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  eqeltrrid  2294  csbexga  4180  rabexd  4197  otexg  4282  tpexg  4499  dmresexg  4991  f1oabexg  5546  funfvex  5606  riotaexg  5916  riotaprop  5936  fnovex  5990  ovexg  5991  fovcdm  6102  fnovrn  6107  cofunexg  6207  cofunex2g  6208  abrexex2g  6218  xpexgALT  6231  mpofvex  6304  tfrex  6467  frec0g  6496  freccllem  6501  ecexg  6637  qsexg  6691  pmex  6753  elixpsn  6835  diffifi  7006  unfidisj  7034  prfidisj  7039  tpfidisj  7041  tpfidceq  7042  ssfirab  7048  ssfidc  7049  fnfi  7053  funrnfi  7059  iunfidisj  7063  infclti  7140  supex2g  7150  infex2g  7151  djuex  7160  ctssdccl  7228  addvalex  7977  negcl  8292  intqfrac2  10486  intfracq  10487  frec2uzzd  10567  frecuzrdgrrn  10575  iseqf1olemqpcl  10676  seq3f1olemqsum  10680  seqf1oglem1  10686  seqf1oglem2  10687  bcval5  10930  xrmaxiflemval  11636  climmpt  11686  reccn2ap  11699  zsumdc  11770  fsumzcl2  11791  fsump1i  11819  fsumabs  11851  hash2iun1dif1  11866  mertenslemi1  11921  fprodcllemf  11999  bitsfzolem  12340  nninfctlemfo  12436  algrf  12442  algcvg  12445  algcvga  12448  algfx  12449  eucalgcvga  12455  eucalg  12456  crth  12621  phimullem  12622  eulerthlemth  12629  prmdiv  12632  pythagtriplem11  12672  pythagtriplem13  12674  pcprecl  12687  infpnlem1  12757  infpnlem2  12758  4sqlem5  12780  mul4sqlem  12791  4sqlemafi  12793  4sqlem13m  12801  4sqlem14  12802  4sqlem17  12805  4sqlem18  12806  ennnfonelemj0  12847  ennnfonelemom  12854  ressbasid  12977  ressval3d  12979  1strbas  13024  2strbasg  13027  2stropg  13028  restid  13157  topnvalg  13158  topnidg  13159  prdsval  13180  prdsplusg  13184  prdsmulr  13185  pwsval  13198  pwselbasb  13200  pwssnf1o  13205  imasival  13213  imasmulr  13216  imasaddfn  13224  imasaddval  13225  imasaddf  13226  imasmulfn  13227  imasmulval  13228  imasmulf  13229  qusval  13230  qusaddval  13242  qusaddf  13243  qusmulval  13244  qusmulf  13245  xpsval  13259  plusffvalg  13269  plusfvalg  13270  grpidvalg  13280  igsumvalx  13296  gsumfzval  13298  gsum0g  13303  gsumsplit1r  13305  gsumprval  13306  prdssgrpd  13322  issubmnd  13349  ress0g  13350  ismhm  13368  0mhm  13393  grpinvfvalg  13449  grpinvval  13450  grpinvfng  13451  grpsubfvalg  13452  grpsubval  13453  grpressid  13468  grplactfval  13508  prdsinvlem  13515  mulgfvalg  13532  mulgval  13533  mulgfng  13535  mulgnngsum  13538  mulgnnp1  13541  mulgnndir  13562  issubg  13584  subggrp  13588  issubg2m  13600  eqgfval  13633  eqgen  13638  quselbasg  13641  quseccl0g  13642  isghm  13654  ghmima  13676  ablressid  13746  gsumfzmptfidmadd  13750  mgpvalg  13760  mgpplusgg  13761  mgptopng  13766  mgpress  13768  rngressid  13791  issrg  13802  ringidss  13866  ring1  13896  ringressid  13900  opprvalg  13906  opprmulfvalg  13907  rdivmuldivd  13981  isnzr2  14021  issubrg  14058  subrgring  14061  rrgval  14099  islmod  14128  scaffvalg  14143  scafvalg  14144  lsssetm  14193  islssm  14194  islssmg  14195  lss1d  14220  lspfval  14225  lspval  14227  lspcl  14228  ellspsn  14254  rnglidlmmgm  14333  rnglidlmsgrp  14334  2idlval  14339  2idlvalg  14340  qusrhm  14365  zlmval  14464  zlmvscag  14470  znval  14473  znle  14474  znbaslemnn  14476  znbas  14481  znzrhval  14484  znleval  14490  psrval  14503  psrbasg  14511  psrelbas  14512  psrplusgg  14515  mplvalcoe  14527  mplbascoe  14528  mplplusgg  14540  topopn  14555  topcld  14656  uncld  14660  iuncld  14662  unicld  14663  tgrest  14716  restin  14723  cnco  14768  cnrest  14782  cnptoprest2  14787  lmss  14793  txbasval  14814  txcn  14822  cnmpt12f  14833  hmeoco  14863  idhmeo  14864  blres  14981  metrest  15053  qtopbasss  15068  tgqioo  15102  divcnap  15112  fsumcncntop  15114  cncfmet  15139  sub1cncf  15149  sub2cncf  15150  cdivcncfap  15151  cnrehmeocntop  15157  cnplimcim  15214  limccnpcntop  15222  limccnp2lem  15223  limccnp2cntop  15224  dvfvalap  15228  dvidsslem  15240  dvmptfsum  15272  plyid  15293  fsumdvdsmul  15538  gausslemma2dlem0b  15602  gausslemma2dlem0d  15604  gausslemma2dlem0h  15608  gausslemma2dlem5a  15617  gausslemma2dlem5  15618  gausslemma2dlem6  15619  lgseisenlem1  15622  lgseisenlem2  15623  lgseisenlem3  15624  lgseisenlem4  15625  2lgslem2  15644  2sqlem8  15675  struct2slots2dom  15712  structiedg0val  15714  edgstruct  15735  uhgrunop  15758  incistruhgr  15761  upgrunop  15793  umgrunop  15795  bj-snexg  15986  trilpolemcl  16117