Theorem eqeltrdi 2847

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  eqeltrrdi  2848  csbexg  5229  unisn2  5231  class2set  5271  snexALT  5301  snex  5349  prex  5350  iotaex  6398  fvrn0  6784  f0cli  6956  funsneqopb  7006  fmptsng  7022  fmptsnd  7023  elimdelov  7349  ovima0  7429  ndmovcl  7435  caovmo  7487  soex  7742  zfrep6  7771  1st2ndb  7844  fprresex  8097  wfrlem17OLD  8127  smofvon2  8158  tz7.44-2  8209  oesuclem  8317  omcl  8328  oecl  8329  nnmcl  8405  nnecl  8406  fsetex  8602  fsetexb  8610  ixpexg  8668  resixpfo  8682  en1bOLD  8768  xpsnen  8796  ssfi  8918  imafi  8920  cnvfi  8924  nnunifi  8995  xpfi  9015  fsuppun  9077  0fsupp  9080  oiexg  9224  hartogslem1  9231  cantnfvalf  9353  rankdmr1  9490  rankr1c  9510  numwdom  9746  alephon  9756  isfin5  9986  sdom2en01  9989  isf32lem9  10048  hsmexlem9  10112  iundom2g  10227  gchxpidm  10356  r1tskina  10469  tskmcl  10528  recmulnq  10651  recclnq  10653  genpelv  10687  un0mulcl  12197  znegcl  12285  zeo  12336  eqreznegel  12603  xnegcl  12876  xnn0xaddcl  12898  ioorebas  13112  modid0  13545  2txmodxeq0  13579  fzofi  13622  seqexw  13665  expcllem  13721  m1expcl2  13732  faclbnd4lem3  13937  bccl  13964  hasheq0  14006  hashrabrsn  14015  fnfz0hashnn0  14088  fnfzo0hashnn0  14091  wrdnfi  14179  ccat2s1p1OLD  14266  cshwcl  14439  relexpaddg  14692  abs00bd  14931  iserge0  15300  sumrblem  15351  fsumcvg  15352  summolem2a  15355  sumss  15364  fsumss  15365  fsumcvg2  15367  sumsplit  15408  binom  15470  bcxmas  15475  geomulcvg  15516  prodrblem  15567  fprodcvg  15568  prodmolem2a  15572  zprod  15575  fprodntriv  15580  prodss  15585  fprodss  15586  binomfallfac  15679  bpoly1  15689  bpoly2  15695  bpoly3  15696  ruclem6  15872  smupf  16113  gcdcl  16141  lcmcl  16234  lcmfcl  16261  2mulprm  16326  pcxnn0cl  16489  pcxcl  16490  pcmptcl  16520  infpnlem2  16540  zgz  16562  4sqlem2  16578  4sqlem19  16592  vdwapval  16602  hashbc0  16634  ramcl2  16645  0ramcl  16652  ramcl  16658  isstruct2  16778  imasval  17139  imasbas  17140  imasds  17141  imasplusg  17145  imasmulr  17146  imasvsca  17148  imasip  17149  imasle  17151  qusaddvallem  17179  qusaddflem  17180  qusaddval  17181  qusaddf  17182  qusmulval  17183  qusmulf  17184  mreexexlem3d  17272  sscpwex  17444  fullresc  17482  estrres  17772  evlfcl  17856  ipopos  18169  gsumress  18281  submnd0  18329  qusgrp2  18608  mulgfval  18617  issubg2  18685  triv1nsgd  18716  torsubg  19370  frgpnabllem1  19389  lt6abl  19411  ablfaclem3  19605  ablfac2  19607  simpgnsgd  19618  srgbinomlem3  19693  ringidss  19731  qusring2  19774  isdrngd  19931  mptscmfsupp0  20103  islss3  20136  lspsnel  20180  lspprel  20271  znf1o  20671  frgpcyg  20693  cnmsgnsubg  20694  phlpropd  20772  cssval  20799  iscss  20800  dsmm0cl  20857  uvcvvcl  20904  m1detdiag  21654  m2detleiblem1  21681  pmatcollpw3fi1lem1  21843  indistopon  22059  indiscld  22150  restbas  22217  ordttopon  22252  iocpnfordt  22274  icomnfordt  22275  lecldbas  22278  fiuncmp  22463  cmpfi  22467  conncompid  22490  dissnlocfin  22588  elpt  22631  xkotop  22647  xkouni  22658  xkohaus  22712  xkoptsub  22713  imastopn  22779  filconn  22942  cfinufil  22987  alexsublem  23103  alexsub  23104  alexsubALTlem4  23109  distgp  23158  indistgp  23159  ssblps  23483  ssbl  23484  xmeter  23494  nmoi  23798  nmoeq0  23806  0nghm  23811  idnghm  23813  icccld  23836  iocmnfcld  23838  blssioo  23864  xrtgioo  23875  xrsxmet  23878  icccmp  23894  pcopt  24091  pcopt2  24092  elpi1  24114  cmetcaulem  24357  ishl2  24439  rrxmvallem  24473  ovolcl  24547  ovolunlem1a  24565  ovolunnul  24569  ovoliunnul  24576  ioombl1  24631  icombl  24633  ioombl  24634  iccmbl  24635  iccvolcl  24636  ovolioo  24637  ioovolcl  24639  ioorcl  24646  uniioovol  24648  uniioombllem2a  24651  uniioombllem4  24655  uniioombllem5  24656  vitalilem1  24677  vitalilem5  24681  mbfconstlem  24696  mbfima  24699  mbfid  24704  ismbf2d  24709  mbfss  24715  mbfmulc2lem  24716  i1fd  24750  itg1addlem2  24766  itg1addlem4  24768  itg1addlem4OLD  24769  itg1addlem5  24770  i1fmulc  24773  itg2l  24799  itg2cl  24802  ibl0  24856  iblrelem  24860  iblpos  24862  iblss2  24875  bddmulibl  24908  bddiblnc  24911  recnperf  24974  ply1remlem  25232  fta1glem1  25235  fta1g  25237  elply  25261  plypf1  25278  coefv0  25314  coemulc  25321  fta1  25373  elqaalem2  25385  aannenlem2  25394  aalioulem3  25399  taylfvallem1  25421  tayl0  25426  ulm0  25455  logtayl  25720  atanrecl  25966  atanbnd  25981  harmonicbnd3  26062  ftalem7  26133  basellem5  26139  ppifi  26160  sqff1o  26236  1sgmprm  26252  logexprlim  26278  dchrelbasd  26292  dchr1re  26316  lgslem4  26353  lgsne0  26388  2sqlem9  26480  2sqlem10  26481  rpvmasumlem  26540  dchrisumlem1  26542  vmalogdivsum  26592  pntrlog2bndlem5  26634  ostth  26692  tgcgr4  26796  axlowdimlem16  27228  fusgrfisbase  27598  vtxdg0e  27744  rgrusgrprc  27859  wwlksnfi  28172  trlsegvdeglem7  28491  eulerpathpr  28505  0blo  29055  nmlno0lem  29056  omlsilem  29665  pjoc1i  29694  nonbooli  29914  nmlnop0iALT  30258  unopbd  30278  leoprf2  30390  opsqrlem4  30406  opsqrlem5  30407  pjbdlni  30412  pjcmul1i  30464  zarcmplem  31733  prsssdm  31769  ordtrestNEW  31773  esumpad  31923  esumpad2  31924  esumcst  31931  esumrnmpt2  31936  sibf0  32201  sitgclcn  32211  sitgclre  32212  eulerpartlemgs2  32247  dstfrvclim1  32344  ballotlemfelz  32357  sgncl  32405  signstfveq0  32456  breprexp  32513  subfacp1lem3  33044  rellysconn  33113  cvmlift2lem9  33173  nnuni  33595  rnttrcl  33708  ttrclse  33713  lrrecse  34026  ordcmp  34563  finxpreclem4  35492  poimirlem16  35720  poimirlem17  35721  voliunnfl  35748  mbfresfi  35750  itg2addnclem2  35756  dvasin  35788  heiborlem4  35899  heiborlem6  35901  sn-iotaex  40123  itrere  40357  retire  40358  wepwsolem  40783  flcidc  40915  iocmbl  40960  arearect  40962  iscard4  41038  briunov2uz  41195  eliunov2uz  41196  frege124d  41258  frege129d  41260  frege92  41452  lhe4.4ex1a  41836  dvconstbi  41841  binomcxplemnn0  41856  binomcxplemnotnn0  41863  infxr  42796  infleinflem2  42800  climneg  43041  cncfiooicc  43325  itgsinexplem1  43385  volioof  43418  stoweidlem36  43467  wallispilem3  43498  fourierdlem93  43630  fouriersw  43662  fouriercn  43663  etransclem16  43681  etransclem33  43698  sge0reuz  43875  nnfoctbdjlem  43883  hoidmvlelem3  44025  dfatafv2ex  44592  sprsymrelfvlem  44830  fmtnofz04prm  44917  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  lincext2  45684  blennn0elnn  45811  itcovalsucov  45902  prstcprs  46242