Theorem eqeltrid 2325

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eqeltrrid  2326  csbexga  4261  rabexd  4281  otexg  4370  tpexg  4590  dmresexg  5086  f1oabexg  5651  funfvex  5712  elfvfvex  5730  riotaexg  6042  riotaeqimp  6063  riotaprop  6064  fnovex  6118  ovexg  6119  elovimad  6129  fovcdm  6232  fnovrn  6237  cofunexg  6338  cofunex2g  6339  abrexex2g  6349  xpexgALT  6366  mpofvex  6441  mptsuppdifd  6495  tfrex  6639  frec0g  6668  freccllem  6673  ecexg  6811  qsexg  6865  pmex  6927  elixpsn  7017  diffifi  7198  unfidisj  7229  prfidisj  7234  tpfidisj  7236  tpfidceq  7237  ssfirab  7244  ssfidc  7245  fnfi  7250  funrnfi  7256  iunfidisj  7260  infclti  7364  supex2g  7374  infex2g  7375  djuex  7384  ctssdccl  7452  addvalex  8212  negcl  8528  intqfrac2  10771  intfracq  10772  frec2uzzd  10852  frecuzrdgrrn  10860  iseqf1olemqpcl  10961  seq3f1olemqsum  10965  seqf1oglem1  10971  seqf1oglem2  10972  bcval5  11217  hashf1lem2  11302  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccatin12  11521  pfxccat3  11522  pfxccatpfx2  11525  pfxccat3a  11526  swrdccat3blem  11527  swrdccat3b  11528  cats1cld  11551  xrmaxiflemval  12035  climmpt  12085  reccn2ap  12098  zsumdc  12170  fsumzcl2  12191  fsump1i  12219  fsumabs  12251  hash2iun1dif1  12266  mertenslemi1  12321  fprodcllemf  12399  bitsfzolem  12740  nninfctlemfo  12836  algrf  12842  algcvg  12845  algcvga  12848  algfx  12849  eucalgcvga  12855  eucalg  12856  crth  13025  phimullem  13026  eulerthlemth  13033  prmdiv  13036  pythagtriplem11  13076  pythagtriplem13  13078  pcprecl  13091  infpnlem1  13161  infpnlem2  13162  4sqlem5  13184  mul4sqlem  13195  4sqlemafi  13197  4sqlem13m  13205  4sqlem14  13206  4sqlem17  13209  4sqlem18  13210  ennnfonelemj0  13344  ennnfonelemom  13351  ressbasid  13477  ressval3d  13479  1strbas  13524  2strbasg  13527  2stropg  13528  restid  13657  topnvalg  13658  topnidg  13659  imasival  13680  imasmulr  13683  imasaddfn  13691  imasaddval  13692  imasaddf  13693  imasmulfn  13694  imasmulval  13695  imasmulf  13696  qusval  13697  qusaddval  13709  qusaddf  13710  qusmulval  13711  qusmulf  13712  plusffvalg  13735  plusfvalg  13736  grpidvalg  13746  gzsumvalx  13762  gzsumfzval  13764  gzsum0  13766  gzsumsplit1r  13768  issubmnd  13808  ress0g  13809  ismhm  13821  0mhm  13846  grpinvfvalg  13900  grpinvval  13901  grpinvfng  13902  grpsubfvalg  13903  grpsubval  13904  grpressid  13919  grplactfval  13959  mulgfvalg  13977  mulgval  13978  mulgfng  13980  mulgnngzsum  13983  mulgnnp1  13986  mulgnndir  14007  issubg  14029  subggrp  14033  issubg2m  14045  eqgfval  14078  eqgen  14083  quselbasg  14086  quseccl0g  14087  isghm  14099  ghmima  14121  cntzex  14144  cntrval  14145  cntzfval  14146  cntzval  14147  cntrnsg  14170  ablressid  14223  gzsumshift  14233  gsumclfi  14243  gsumsubmclfi  14247  prdsval  14257  prdsplusg  14261  prdsmulr  14262  prdssgrpd  14275  prdsinvlem  14280  xpsval  14285  pwsval  14288  pwselbasb  14290  pwssnf1o  14295  mgpvalg  14304  mgpplusgg  14305  mgptopng  14312  mgpress  14314  rngressid  14337  issrg  14353  ringidss  14418  ring1  14448  ringressid  14452  opprvalg  14458  opprmulfvalg  14459  rdivmuldivd  14535  isnzr2  14575  issubrg  14613  subrgring  14616  rrgval  14654  islmod  14711  scaffvalg  14727  scafvalg  14728  lsssetm  14777  islssm  14778  islssmg  14779  lss1d  14804  lspfval  14809  lspval  14811  lspcl  14812  ellspsn  14838  rnglidlmmgm  14917  rnglidlmsgrp  14918  2idlval  14923  2idlvalg  14924  qusrhm  14949  zlmval  15046  zlmvscag  15052  znval  15055  znle  15056  znbaslemnn  15058  znbas  15063  znzrhval  15066  znleval  15072  aspval  15099  asclfval  15105  psrval  15134  psrbasg  15150  psrelbas  15151  psrplusgg  15154  psrmulrg  15158  mplvalcoe  15172  mplbascoe  15173  mplplusgg  15185  topopn  15200  topcld  15301  uncld  15305  iuncld  15307  unicld  15308  tgrest  15361  restin  15368  cnco  15413  cnrest  15427  cnptoprest2  15432  lmss  15438  txbasval  15459  txcn  15467  cnmpt12f  15478  hmeoco  15508  idhmeo  15509  blres  15626  metrest  15698  qtopbasss  15713  tgqioo  15747  divcnap  15757  fsumcncntop  15759  cncfmet  15784  sub1cncf  15794  sub2cncf  15795  cdivcncfap  15796  cnrehmeocntop  15802  cnplimcim  15859  limccnpcntop  15867  limccnp2lem  15868  limccnp2cntop  15869  dvfvalap  15873  dvidsslem  15885  dvmptfsum  15917  plyid  15938  logfac  16090  fsumdvdsmul  16246  bposlem3  16274  bposlem5  16276  bposlem6  16277  gausslemma2dlem0b  16335  gausslemma2dlem0d  16337  gausslemma2dlem0h  16341  gausslemma2dlem5a  16350  gausslemma2dlem5  16351  gausslemma2dlem6  16352  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem3  16357  lgseisenlem4  16358  2lgslem2  16377  2sqlem8  16408  struct2slots2dom  16445  structiedg0val  16447  edgstruct  16471  uhgrunop  16494  incistruhgr  16497  upgrunop  16534  umgrunop  16536  usgredg2v  16631  usgriedgdomord  16632  uspgredgdomord  16636  subgruhgredgdm  16677  uhgrspansubgrlem  16683  uhgrspanop  16689  upgrspanop  16690  umgrspanop  16691  usgrspanop  16692  vtxdgfval  16695  wksfval  16729  wlk1walkdom  16766  clwwlkg  16800  trlsegvdeglem3  16869  trlsegvdeglem5  16871  eupthvdres  16882  eupth2lem3fi  16883  eupth2lembfi  16884  bj-snexg  17104  trilpolemcl  17253