Theorem eqeltrdi 2877

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
eqeltrdi.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqeltrdi.2	⊢ 𝐵 ∈ 𝐶

Assertion

Ref	Expression
eqeltrdi	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eqeltrdi

Step	Hyp	Ref	Expression
1		eqeltrdi.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqeltrdi.2	. . 3 ⊢ 𝐵 ∈ 𝐶
3	2	a1i 11	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	1, 3	eqeltrd 2869	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  eqeltrrdi  2878  csbexg  5275  unisn2  5277  class2set  5326  snexALT  5355  snexOLD  5414  prexOLD  5415  iotaex  6513  fvrn0  6910  f0cli  7094  funsneqopb  7150  fmptsng  7167  fmptsnd  7168  elimdelov  7507  ovima0  7590  ndmovcl  7596  caovmo  7648  soex  7917  zfrep6OLD  7951  1st2ndb  8025  fprresex  8306  smofvon2  8342  tz7.44-2  8393  oesuclem  8509  omcl  8520  oecl  8521  nnmcl  8597  nnecl  8598  fsetex  8852  fsetexb  8860  ixpexg  8919  resixpfo  8933  xpsnen  9048  ssfi  9156  cnvfi  9159  nnunifi  9250  prfi  9282  fsuppun  9346  0fsupp  9349  oiexg  9496  hartogslem1  9503  cantnfvalf  9633  rnttrcl  9690  ttrclse  9695  rankdmr1  9772  rankr1c  9792  numwdom  10042  alephon  10052  isfin5  10282  sdom2en01  10285  isf32lem9  10344  hsmexlem9  10408  iundom2g  10523  gchxpidm  10653  r1tskina  10766  tskmcl  10825  recmulnq  10948  recclnq  10950  genpelv  10984  un0mulcl  12537  znegcl  12628  zeo  12681  eqreznegel  12957  xnegcl  13238  xnn0xaddcl  13260  ioorebas  13477  modid0  13929  2txmodxeq0  13966  fzofi  14009  seqexw  14052  expcllem  14107  m1expcl2  14120  faclbnd4lem3  14330  bccl  14357  hasheq0  14398  hashrabrsn  14407  fnfz0hashnn0  14484  fnfzo0hashnn0  14487  wrdnfi  14584  cshwcl  14834  relexpaddg  15089  sgncl  15133  abs00bd  15341  iserge0  15711  sumrblem  15761  fsumcvg  15762  summolem2a  15765  sumss  15774  fsumss  15775  fsumcvg2  15777  sumsplit  15818  binom  15883  bcxmas  15888  geomulcvg  15929  prodrblem  15982  fprodcvg  15983  prodmolem2a  15987  zprod  15990  fprodntriv  15995  prodss  16000  fprodss  16001  binomfallfac  16094  bpoly1  16104  bpoly2  16110  bpoly3  16111  ruclem6  16290  smupf  16535  gcdcl  16563  lcmcl  16658  lcmfcl  16685  2mulprm  16750  pcxnn0cl  16919  pcxcl  16920  pcmptcl  16950  infpnlem2  16970  zgz  16992  4sqlem2  17008  4sqlem19  17022  vdwapval  17032  hashbc0  17064  ramcl2  17075  0ramcl  17082  ramcl  17088  isstruct2  17208  imasval  17564  imasbas  17565  imasds  17566  imasplusg  17570  imasmulr  17571  imasvsca  17573  imasip  17574  imasle  17576  qusaddvallem  17604  qusaddflem  17605  qusaddval  17606  qusaddf  17607  qusmulval  17608  qusmulf  17609  mreexexlem3d  17701  sscpwex  17871  fullresc  17907  estrres  18194  evlfcl  18277  ipopos  18591  gsumress  18739  submnd0  18820  qusgrp2  19123  mulgfval  19134  issubg2  19207  triv1nsgd  19238  0subgALT  19637  torsubg  19923  frgpnabllem1  19942  lt6abl  19964  ablfaclem3  20158  ablfac2  20160  simpgnsgd  20171  qusrng  20257  srgbinomlem3  20309  ringidss  20359  qusring2  20415  isdrngd  20846  isdrngdOLD  20848  mptscmfsupp0  21025  islss3  21057  ellspsn  21101  lspprel  21192  znf1o  21669  frgpcyg  21691  cnmsgnsubg  21695  phlpropd  21773  cssval  21800  iscss  21801  dsmm0cl  21858  uvcvvcl  21905  m1detdiag  22722  m2detleiblem1  22749  pmatcollpw3fi1lem1  22911  indistopon  23126  indiscld  23216  restbas  23283  ordttopon  23318  iocpnfordt  23340  icomnfordt  23341  lecldbas  23344  fiuncmp  23529  cmpfi  23533  conncompid  23556  dissnlocfin  23654  elpt  23697  xkotop  23713  xkouni  23724  xkohaus  23778  xkoptsub  23779  imastopn  23845  filconn  24008  cfinufil  24053  alexsublem  24169  alexsub  24170  alexsubALTlem4  24175  distgp  24224  indistgp  24225  ssblps  24547  ssbl  24548  xmeter  24558  nmoi  24853  nmoeq0  24861  0nghm  24866  idnghm  24868  icccld  24891  iocmnfcld  24893  blssioo  24920  xrtgioo  24932  xrsxmet  24935  icccmp  24951  pcopt  25149  pcopt2  25150  elpi1  25172  cmetcaulem  25415  ishl2  25497  rrxmvallem  25531  ovolcl  25605  ovolunlem1a  25623  ovolunnul  25627  ovoliunnul  25634  ioombl1  25689  icombl  25691  ioombl  25692  iccmbl  25693  iccvolcl  25694  ovolioo  25695  ioovolcl  25697  ioorcl  25704  uniioovol  25706  uniioombllem2a  25709  uniioombllem4  25713  uniioombllem5  25714  vitalilem1  25735  vitalilem5  25739  mbfconstlem  25754  mbfima  25757  mbfid  25762  ismbf2d  25767  mbfss  25773  mbfmulc2lem  25774  i1fd  25808  itg1addlem2  25824  itg1addlem4  25826  itg1addlem5  25827  i1fmulc  25830  itg2l  25856  itg2cl  25859  ibl0  25914  iblrelem  25918  iblpos  25920  iblss2  25933  bddmulibl  25966  bddiblnc  25969  recnperf  26032  ply1remlem  26290  fta1glem1  26293  fta1g  26295  elply  26320  plypf1  26337  coefv0  26373  coemulc  26380  fta1  26437  elqaalem2  26449  aannenlem2  26458  aalioulem3  26463  taylfvallem1  26485  tayl0  26490  ulm0  26519  logtayl  26790  atanrecl  27041  atanbnd  27056  harmonicbnd3  27137  ftalem7  27208  basellem5  27214  ppifi  27235  sqff1o  27311  1sgmprm  27328  logexprlim  27354  dchrelbasd  27368  dchr1re  27392  lgslem4  27429  lgsne0  27464  2sqlem9  27556  2sqlem10  27557  rpvmasumlem  27616  dchrisumlem1  27618  vmalogdivsum  27668  pntrlog2bndlem5  27710  ostth  27768  lrrecse  28100  sltmuls1  28305  sltmuls2  28306  mulsuniflem  28307  noseqex  28447  n0mulscl  28503  n0fincut  28513  eln0s  28519  n0subs  28521  n0zs  28547  expscllem  28588  elz12s  28630  tgcgr4  28765  axlowdimlem16  29247  fusgrfisbase  29618  vtxdg0e  29764  rgrusgrprc  29879  wwlksnfi  30195  trlsegvdeglem7  30517  eulerpathpr  30531  0blo  31084  nmlno0lem  31085  omlsilem  31694  pjoc1i  31723  nonbooli  31943  nmlnop0iALT  32287  unopbd  32307  leoprf2  32419  opsqrlem4  32435  opsqrlem5  32436  pjbdlni  32441  pjcmul1i  32493  mptiffisupp  32978  drngidlhash  33685  evl1deg1  33810  ply1dg1rt  33814  ply1dg3rt0irred  33818  m1pmeq  33819  mplmulmvr  33873  esplyfvaln  33908  vieta  33914  lvecendof1f1o  33967  fldext2rspun  34016  constrabscl  34112  zarcmplem  34215  prsssdm  34251  ordtrestNEW  34255  esumpad  34389  esumpad2  34390  esumcst  34397  esumrnmpt2  34402  sibf0  34668  sitgclcn  34678  sitgclre  34679  eulerpartlemgs2  34714  dstfrvclim1  34812  ballotlemfelz  34825  signstfveq0  34908  breprexp  34964  r1wf  35431  fineqvnttrclselem1  35456  wevgblacfn  35493  subfacp1lem3  35572  rellysconn  35641  cvmlift2lem9  35701  nnuni  36117  ordcmp  36846  bj-snex  37558  finxpreclem4  37927  poimirlem16  38174  poimirlem17  38175  voliunnfl  38202  mbfresfi  38204  itg2addnclem2  38210  dvasin  38242  heiborlem4  38352  heiborlem6  38354  25or6to4  42862  itrere  42968  sn-itrere  43151  sn-retire  43152  wepwsolem  43660  flcidc  43788  iocmbl  43831  arearect  43833  omcl3g  43952  iscard4  44150  briunov2uz  44315  eliunov2uz  44316  frege124d  44378  frege129d  44380  frege92  44572  lhe4.4ex1a  44930  dvconstbi  44935  binomcxplemnn0  44950  binomcxplemnotnn0  44957  infxr  45973  infleinflem2  45977  climneg  46217  cncfiooicc  46499  itgsinexplem1  46559  volioof  46592  stoweidlem36  46641  wallispilem3  46672  fourierdlem93  46804  fouriersw  46836  fouriercn  46837  etransclem16  46855  etransclem33  46872  sge0reuz  47052  nnfoctbdjlem  47060  hoidmvlelem3  47202  sinnpoly  47516  dfatafv2ex  47838  sprsymrelfvlem  48127  fmtnofz04prm  48217  nnsum4primeseven  48453  nnsum4primesevenALTV  48454  gpg3nbgrvtx0  48729  lincext2  49119  blennn0elnn  49241  itcovalsucov  49332  resccat  49736  funcf2lem2  49744  isnatd  49885  swapfelvv  49925  fucoelvv  49982  prcofelvv  50042  termco  50143  prstcprs  50222