Theorem eqeltrdi 2846

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  eqeltrrdi  2847  csbexg  5315  unisn2  5317  class2set  5360  snexALT  5388  snex  5441  prex  5442  iotaex  6535  iotaexOLD  6542  fvrn0  6936  f0cli  7117  funsneqopb  7171  fmptsng  7187  fmptsnd  7188  elimdelov  7528  ovima0  7611  ndmovcl  7617  caovmo  7669  soex  7943  zfrep6  7977  1st2ndb  8052  fprresex  8333  wfrlem17OLD  8363  smofvon2  8394  tz7.44-2  8445  oesuclem  8561  omcl  8572  oecl  8573  nnmcl  8648  nnecl  8649  fsetex  8894  fsetexb  8902  ixpexg  8960  resixpfo  8974  xpsnen  9093  ssfi  9211  cnvfi  9214  nnunifi  9324  imafiOLD  9351  xpfiOLD  9356  prfi  9360  fsuppun  9424  0fsupp  9427  oiexg  9572  hartogslem1  9579  cantnfvalf  9702  rnttrcl  9759  ttrclse  9764  rankdmr1  9838  rankr1c  9858  numwdom  10096  alephon  10106  isfin5  10336  sdom2en01  10339  isf32lem9  10398  hsmexlem9  10462  iundom2g  10577  gchxpidm  10706  r1tskina  10819  tskmcl  10878  recmulnq  11001  recclnq  11003  genpelv  11037  un0mulcl  12557  znegcl  12649  zeo  12701  eqreznegel  12973  xnegcl  13251  xnn0xaddcl  13273  ioorebas  13487  modid0  13933  2txmodxeq0  13968  fzofi  14011  seqexw  14054  expcllem  14109  m1expcl2  14122  faclbnd4lem3  14330  bccl  14357  hasheq0  14398  hashrabrsn  14407  fnfz0hashnn0  14483  fnfzo0hashnn0  14486  wrdnfi  14582  cshwcl  14832  relexpaddg  15088  abs00bd  15326  iserge0  15693  sumrblem  15743  fsumcvg  15744  summolem2a  15747  sumss  15756  fsumss  15757  fsumcvg2  15759  sumsplit  15800  binom  15862  bcxmas  15867  geomulcvg  15908  prodrblem  15961  fprodcvg  15962  prodmolem2a  15966  zprod  15969  fprodntriv  15974  prodss  15979  fprodss  15980  binomfallfac  16073  bpoly1  16083  bpoly2  16089  bpoly3  16090  ruclem6  16267  smupf  16511  gcdcl  16539  lcmcl  16634  lcmfcl  16661  2mulprm  16726  pcxnn0cl  16893  pcxcl  16894  pcmptcl  16924  infpnlem2  16944  zgz  16966  4sqlem2  16982  4sqlem19  16996  vdwapval  17006  hashbc0  17038  ramcl2  17049  0ramcl  17056  ramcl  17062  isstruct2  17182  imasval  17557  imasbas  17558  imasds  17559  imasplusg  17563  imasmulr  17564  imasvsca  17566  imasip  17567  imasle  17569  qusaddvallem  17597  qusaddflem  17598  qusaddval  17599  qusaddf  17600  qusmulval  17601  qusmulf  17602  mreexexlem3d  17690  sscpwex  17862  fullresc  17901  estrres  18194  evlfcl  18278  ipopos  18593  gsumress  18707  submnd0  18788  qusgrp2  19088  mulgfval  19099  issubg2  19171  triv1nsgd  19203  0subgALT  19600  torsubg  19886  frgpnabllem1  19905  lt6abl  19927  ablfaclem3  20121  ablfac2  20123  simpgnsgd  20134  qusrng  20197  srgbinomlem3  20245  ringidss  20290  qusring2  20347  isdrngd  20781  isdrngdOLD  20783  mptscmfsupp0  20941  islss3  20974  ellspsn  21018  lspprel  21110  znf1o  21587  frgpcyg  21609  cnmsgnsubg  21612  phlpropd  21690  cssval  21717  iscss  21718  dsmm0cl  21777  uvcvvcl  21824  m1detdiag  22618  m2detleiblem1  22645  pmatcollpw3fi1lem1  22807  indistopon  23023  indiscld  23114  restbas  23181  ordttopon  23216  iocpnfordt  23238  icomnfordt  23239  lecldbas  23242  fiuncmp  23427  cmpfi  23431  conncompid  23454  dissnlocfin  23552  elpt  23595  xkotop  23611  xkouni  23622  xkohaus  23676  xkoptsub  23677  imastopn  23743  filconn  23906  cfinufil  23951  alexsublem  24067  alexsub  24068  alexsubALTlem4  24073  distgp  24122  indistgp  24123  ssblps  24447  ssbl  24448  xmeter  24458  nmoi  24764  nmoeq0  24772  0nghm  24777  idnghm  24779  icccld  24802  iocmnfcld  24804  blssioo  24830  xrtgioo  24841  xrsxmet  24844  icccmp  24860  pcopt  25068  pcopt2  25069  elpi1  25091  cmetcaulem  25335  ishl2  25417  rrxmvallem  25451  ovolcl  25526  ovolunlem1a  25544  ovolunnul  25548  ovoliunnul  25555  ioombl1  25610  icombl  25612  ioombl  25613  iccmbl  25614  iccvolcl  25615  ovolioo  25616  ioovolcl  25618  ioorcl  25625  uniioovol  25627  uniioombllem2a  25630  uniioombllem4  25634  uniioombllem5  25635  vitalilem1  25656  vitalilem5  25660  mbfconstlem  25675  mbfima  25678  mbfid  25683  ismbf2d  25688  mbfss  25694  mbfmulc2lem  25695  i1fd  25729  itg1addlem2  25745  itg1addlem4  25747  itg1addlem4OLD  25748  itg1addlem5  25749  i1fmulc  25752  itg2l  25778  itg2cl  25781  ibl0  25836  iblrelem  25840  iblpos  25842  iblss2  25855  bddmulibl  25888  bddiblnc  25891  recnperf  25954  ply1remlem  26218  fta1glem1  26221  fta1g  26223  elply  26248  plypf1  26265  coefv0  26301  coemulc  26308  fta1  26364  elqaalem2  26376  aannenlem2  26385  aalioulem3  26390  taylfvallem1  26412  tayl0  26417  ulm0  26448  logtayl  26716  atanrecl  26968  atanbnd  26983  harmonicbnd3  27065  ftalem7  27136  basellem5  27142  ppifi  27163  sqff1o  27239  1sgmprm  27257  logexprlim  27283  dchrelbasd  27297  dchr1re  27321  lgslem4  27358  lgsne0  27393  2sqlem9  27485  2sqlem10  27486  rpvmasumlem  27545  dchrisumlem1  27547  vmalogdivsum  27597  pntrlog2bndlem5  27639  ostth  27697  lrrecse  27989  ssltmul1  28187  ssltmul2  28188  mulsuniflem  28189  noseqex  28309  n0mulscl  28362  eln0s  28372  n0subs  28374  n0zs  28389  expscl  28427  elzs12  28435  tgcgr4  28553  axlowdimlem16  28986  fusgrfisbase  29359  vtxdg0e  29506  rgrusgrprc  29621  wwlksnfi  29935  trlsegvdeglem7  30254  eulerpathpr  30268  0blo  30820  nmlno0lem  30821  omlsilem  31430  pjoc1i  31459  nonbooli  31679  nmlnop0iALT  32023  unopbd  32043  leoprf2  32155  opsqrlem4  32171  opsqrlem5  32172  pjbdlni  32177  pjcmul1i  32229  mptiffisupp  32707  drngidlhash  33441  evl1deg1  33580  ply1dg1rt  33583  ply1dg3rt0irred  33586  m1pmeq  33587  lvecendof1f1o  33660  zarcmplem  33841  prsssdm  33877  ordtrestNEW  33881  esumpad  34035  esumpad2  34036  esumcst  34043  esumrnmpt2  34048  sibf0  34315  sitgclcn  34325  sitgclre  34326  eulerpartlemgs2  34361  dstfrvclim1  34458  ballotlemfelz  34471  sgncl  34519  signstfveq0  34570  breprexp  34626  wevgblacfn  35092  subfacp1lem3  35166  rellysconn  35235  cvmlift2lem9  35295  nnuni  35706  ordcmp  36429  bj-snex  37017  finxpreclem4  37376  poimirlem16  37622  poimirlem17  37623  voliunnfl  37650  mbfresfi  37652  itg2addnclem2  37658  dvasin  37690  heiborlem4  37800  heiborlem6  37802  itrere  42331  sn-itrere  42474  sn-retire  42475  wepwsolem  43030  flcidc  43158  iocmbl  43201  arearect  43203  omcl3g  43323  iscard4  43522  briunov2uz  43687  eliunov2uz  43688  frege124d  43750  frege129d  43752  frege92  43944  lhe4.4ex1a  44324  dvconstbi  44329  binomcxplemnn0  44344  binomcxplemnotnn0  44351  infxr  45316  infleinflem2  45320  climneg  45565  cncfiooicc  45849  itgsinexplem1  45909  volioof  45942  stoweidlem36  45991  wallispilem3  46022  fourierdlem93  46154  fouriersw  46186  fouriercn  46187  etransclem16  46205  etransclem33  46222  sge0reuz  46402  nnfoctbdjlem  46410  hoidmvlelem3  46552  upwordnul  46833  dfatafv2ex  47162  sprsymrelfvlem  47414  fmtnofz04prm  47501  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  gpg3nbgrvtx0  47966  lincext2  48300  blennn0elnn  48426  itcovalsucov  48517  prstcprs  48875