Theorem eqeltrdi 2841

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810

This theorem is referenced by:  eqeltrrdi  2842  csbexg  5310  unisn2  5312  class2set  5353  snexALT  5381  snex  5431  prex  5432  iotaex  6516  iotaexOLD  6523  fvrn0  6921  f0cli  7099  funsneqopb  7152  fmptsng  7168  fmptsnd  7169  elimdelov  7507  ovima0  7588  ndmovcl  7594  caovmo  7646  soex  7914  zfrep6  7943  1st2ndb  8017  fprresex  8297  wfrlem17OLD  8327  smofvon2  8358  tz7.44-2  8409  oesuclem  8527  omcl  8538  oecl  8539  nnmcl  8614  nnecl  8615  fsetex  8852  fsetexb  8860  ixpexg  8918  resixpfo  8932  en1bOLD  9026  xpsnen  9057  ssfi  9175  imafi  9177  cnvfi  9182  nnunifi  9296  xpfiOLD  9320  fsuppun  9384  0fsupp  9387  oiexg  9532  hartogslem1  9539  cantnfvalf  9662  rnttrcl  9719  ttrclse  9724  rankdmr1  9798  rankr1c  9818  numwdom  10056  alephon  10066  isfin5  10296  sdom2en01  10299  isf32lem9  10358  hsmexlem9  10422  iundom2g  10537  gchxpidm  10666  r1tskina  10779  tskmcl  10838  recmulnq  10961  recclnq  10963  genpelv  10997  un0mulcl  12508  znegcl  12599  zeo  12650  eqreznegel  12920  xnegcl  13194  xnn0xaddcl  13216  ioorebas  13430  modid0  13864  2txmodxeq0  13898  fzofi  13941  seqexw  13984  expcllem  14040  m1expcl2  14053  faclbnd4lem3  14257  bccl  14284  hasheq0  14325  hashrabrsn  14334  fnfz0hashnn0  14409  fnfzo0hashnn0  14412  wrdnfi  14500  cshwcl  14750  relexpaddg  15002  abs00bd  15240  iserge0  15609  sumrblem  15659  fsumcvg  15660  summolem2a  15663  sumss  15672  fsumss  15673  fsumcvg2  15675  sumsplit  15716  binom  15778  bcxmas  15783  geomulcvg  15824  prodrblem  15875  fprodcvg  15876  prodmolem2a  15880  zprod  15883  fprodntriv  15888  prodss  15893  fprodss  15894  binomfallfac  15987  bpoly1  15997  bpoly2  16003  bpoly3  16004  ruclem6  16180  smupf  16421  gcdcl  16449  lcmcl  16540  lcmfcl  16567  2mulprm  16632  pcxnn0cl  16795  pcxcl  16796  pcmptcl  16826  infpnlem2  16846  zgz  16868  4sqlem2  16884  4sqlem19  16898  vdwapval  16908  hashbc0  16940  ramcl2  16951  0ramcl  16958  ramcl  16964  isstruct2  17084  imasval  17459  imasbas  17460  imasds  17461  imasplusg  17465  imasmulr  17466  imasvsca  17468  imasip  17469  imasle  17471  qusaddvallem  17499  qusaddflem  17500  qusaddval  17501  qusaddf  17502  qusmulval  17503  qusmulf  17504  mreexexlem3d  17592  sscpwex  17764  fullresc  17803  estrres  18093  evlfcl  18177  ipopos  18491  gsumress  18603  submnd0  18656  qusgrp2  18943  mulgfval  18954  issubg2  19023  triv1nsgd  19055  0subgALT  19438  torsubg  19724  frgpnabllem1  19743  lt6abl  19765  ablfaclem3  19959  ablfac2  19961  simpgnsgd  19972  srgbinomlem3  20053  ringidss  20096  qusring2  20151  isdrngd  20394  isdrngdOLD  20396  mptscmfsupp0  20542  islss3  20575  lspsnel  20619  lspprel  20710  znf1o  21113  frgpcyg  21135  cnmsgnsubg  21136  phlpropd  21214  cssval  21241  iscss  21242  dsmm0cl  21301  uvcvvcl  21348  m1detdiag  22106  m2detleiblem1  22133  pmatcollpw3fi1lem1  22295  indistopon  22511  indiscld  22602  restbas  22669  ordttopon  22704  iocpnfordt  22726  icomnfordt  22727  lecldbas  22730  fiuncmp  22915  cmpfi  22919  conncompid  22942  dissnlocfin  23040  elpt  23083  xkotop  23099  xkouni  23110  xkohaus  23164  xkoptsub  23165  imastopn  23231  filconn  23394  cfinufil  23439  alexsublem  23555  alexsub  23556  alexsubALTlem4  23561  distgp  23610  indistgp  23611  ssblps  23935  ssbl  23936  xmeter  23946  nmoi  24252  nmoeq0  24260  0nghm  24265  idnghm  24267  icccld  24290  iocmnfcld  24292  blssioo  24318  xrtgioo  24329  xrsxmet  24332  icccmp  24348  pcopt  24545  pcopt2  24546  elpi1  24568  cmetcaulem  24812  ishl2  24894  rrxmvallem  24928  ovolcl  25002  ovolunlem1a  25020  ovolunnul  25024  ovoliunnul  25031  ioombl1  25086  icombl  25088  ioombl  25089  iccmbl  25090  iccvolcl  25091  ovolioo  25092  ioovolcl  25094  ioorcl  25101  uniioovol  25103  uniioombllem2a  25106  uniioombllem4  25110  uniioombllem5  25111  vitalilem1  25132  vitalilem5  25136  mbfconstlem  25151  mbfima  25154  mbfid  25159  ismbf2d  25164  mbfss  25170  mbfmulc2lem  25171  i1fd  25205  itg1addlem2  25221  itg1addlem4  25223  itg1addlem4OLD  25224  itg1addlem5  25225  i1fmulc  25228  itg2l  25254  itg2cl  25257  ibl0  25311  iblrelem  25315  iblpos  25317  iblss2  25330  bddmulibl  25363  bddiblnc  25366  recnperf  25429  ply1remlem  25687  fta1glem1  25690  fta1g  25692  elply  25716  plypf1  25733  coefv0  25769  coemulc  25776  fta1  25828  elqaalem2  25840  aannenlem2  25849  aalioulem3  25854  taylfvallem1  25876  tayl0  25881  ulm0  25910  logtayl  26175  atanrecl  26423  atanbnd  26438  harmonicbnd3  26519  ftalem7  26590  basellem5  26596  ppifi  26617  sqff1o  26693  1sgmprm  26709  logexprlim  26735  dchrelbasd  26749  dchr1re  26773  lgslem4  26810  lgsne0  26845  2sqlem9  26937  2sqlem10  26938  rpvmasumlem  26997  dchrisumlem1  26999  vmalogdivsum  27049  pntrlog2bndlem5  27091  ostth  27149  lrrecse  27435  ssltmul1  27612  ssltmul2  27613  mulsuniflem  27614  tgcgr4  27820  axlowdimlem16  28253  fusgrfisbase  28623  vtxdg0e  28769  rgrusgrprc  28884  wwlksnfi  29198  trlsegvdeglem7  29517  eulerpathpr  29531  0blo  30083  nmlno0lem  30084  omlsilem  30693  pjoc1i  30722  nonbooli  30942  nmlnop0iALT  31286  unopbd  31306  leoprf2  31418  opsqrlem4  31434  opsqrlem5  31435  pjbdlni  31440  pjcmul1i  31492  mptiffisupp  31953  drngidlhash  32597  zarcmplem  32930  prsssdm  32966  ordtrestNEW  32970  esumpad  33122  esumpad2  33123  esumcst  33130  esumrnmpt2  33135  sibf0  33402  sitgclcn  33412  sitgclre  33413  eulerpartlemgs2  33448  dstfrvclim1  33545  ballotlemfelz  33558  sgncl  33606  signstfveq0  33657  breprexp  33714  subfacp1lem3  34242  rellysconn  34311  cvmlift2lem9  34371  nnuni  34765  ordcmp  35418  bj-snex  36002  finxpreclem4  36361  poimirlem16  36590  poimirlem17  36591  voliunnfl  36618  mbfresfi  36620  itg2addnclem2  36626  dvasin  36658  heiborlem4  36768  heiborlem6  36770  itrere  41421  retire  41422  wepwsolem  41866  flcidc  41998  iocmbl  42044  arearect  42046  omcl3g  42166  iscard4  42366  briunov2uz  42531  eliunov2uz  42532  frege124d  42594  frege129d  42596  frege92  42788  lhe4.4ex1a  43170  dvconstbi  43175  binomcxplemnn0  43190  binomcxplemnotnn0  43197  infxr  44156  infleinflem2  44160  climneg  44405  cncfiooicc  44689  itgsinexplem1  44749  volioof  44782  stoweidlem36  44831  wallispilem3  44862  fourierdlem93  44994  fouriersw  45026  fouriercn  45027  etransclem16  45045  etransclem33  45062  sge0reuz  45242  nnfoctbdjlem  45250  hoidmvlelem3  45392  upwordnul  45673  dfatafv2ex  46000  sprsymrelfvlem  46237  fmtnofz04prm  46324  nnsum4primeseven  46547  nnsum4primesevenALTV  46548  qusrng  46760  lincext2  47214  blennn0elnn  47341  itcovalsucov  47432  prstcprs  47773