Theorem eqeltri 2836

Description: Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
eqeltri.1	⊢ 𝐴 = 𝐵
eqeltri.2	⊢ 𝐵 ∈ 𝐶

Assertion

Ref	Expression
eqeltri	⊢ 𝐴 ∈ 𝐶

Proof of Theorem eqeltri

Step	Hyp	Ref	Expression
1		eqeltri.2	. 2 ⊢ 𝐵 ∈ 𝐶
2		eqeltri.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	eleq1i 2830	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)
4	1, 3	mpbir 230	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1541   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

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

This theorem is referenced by:  eqeltrri  2837  3eltr4i  2853  intab  4914  unisn2  5239  inex2  5245  vpwex  5303  ord3ex  5313  zfpair  5347  opex  5381  otex  5382  uniopel  5432  elvvuni  5662  isarep2  6519  fvex  6781  fvexi  6782  riotaex  7229  ovexi  7302  tpex  7588  oprabex  7805  oprabrexex2  7807  mpoexw  7905  tfrlem16  8208  1on  8288  2on  8289  3on  8291  4on  8292  1oex  8294  2oex  8298  2oexOLD  8299  oesuclem  8331  oecl  8343  o2p2e4  8347  nnecl  8420  1onn  8446  2onn  8447  3onn  8448  4onn  8449  mapsnf1o2  8656  sbthlem10  8848  imafi  8923  pwfi  8926  cnvfi  8928  fnfi  8929  nnunifi  9026  xpfi  9046  prfi  9050  tpfi  9051  pwfiOLD  9075  fczfsuppd  9107  cantnfvalf  9384  oemapwe  9413  cantnffval2  9414  cnfcom3clem  9424  ssttrcl  9434  trpredex  9468  r1fin  9515  hta  9639  infxpenlem  9753  alephon  9809  alephfplem1  9844  dfac5lem4  9866  dfac5lem5  9867  kmlem10  9899  fin1a2lem10  10149  fin1a2lem12  10151  hsmexlem9  10165  axcc2lem  10176  domtriomlem  10182  axdc2lem  10188  axcclem  10197  brdom7disj  10271  brdom6disj  10272  iundom2g  10280  konigthlem  10308  canthwelem  10390  wunex2  10478  wunex3  10481  1nq  10668  1pr  10755  nrex1  10804  axcnex  10887  ax1cn  10889  pnfex  11012  mnfxr  11016  inelr  11946  cju  11952  nnexALT  11958  2nn  12029  2re  12030  2cn  12031  3nn  12035  3re  12036  3cn  12037  4nn  12039  4re  12040  4cn  12041  5nn  12042  5re  12043  5cn  12044  6nn  12045  6re  12046  6cn  12047  7nn  12048  7re  12049  7cn  12050  8nn  12051  8re  12052  8cn  12053  9nn  12054  9re  12055  9cn  12056  nn0ex  12222  zexALT  12322  nneo  12387  zeo  12389  deccl  12434  10re  12438  decnncl  12439  numnncl2  12442  decnncl2  12443  numsucc  12459  numma2c  12465  numadd  12466  numaddc  12467  nummul1c  12468  nummul2c  12469  decmul1  12483  qexALT  12686  xrex  12709  xnegex  12924  xnegcl  12929  ixxssxr  13073  om2uzuzi  13650  ltweuz  13662  axdc4uzlem  13684  seqex  13704  seqexw  13718  m1expcl2  13785  faccl  13978  facwordi  13984  faclbnd2  13986  bccl  14017  hashen1  14066  hashrabrsn  14068  hashunlei  14121  hashpw  14132  s1cli  14291  ccat2s1p1  14317  cats1un  14415  revs1  14459  cshwsexa  14518  cats1cli  14551  cats1fvn  14552  crre  14806  remim  14809  climmpt  15261  sumex  15380  supcvg  15549  geo2lim  15568  prodex  15598  bpoly4  15750  ere  15779  eftlub  15799  efsep  15800  tan0  15841  ef01bndlem  15874  nn0o  16073  divalglem5  16087  divalglem9  16091  sadcf  16141  smupf  16166  crth  16460  phimullem  16461  pczpre  16529  pockthi  16589  prmreclem2  16599  igz  16616  0ramcl  16705  1259lem1  16813  1259lem2  16814  1259lem3  16815  1259lem4  16816  1259lem5  16817  1259prm  16818  2503lem1  16819  2503lem2  16820  2503lem3  16821  2503prm  16822  4001lem1  16823  4001lem2  16824  4001lem3  16825  4001lem4  16826  4001prm  16827  strle1  16840  ndxarg  16878  basendxnn  16903  basendxnnOLD  16904  plusgndxnn  16971  tsetndxnn  17045  plendxnn  17059  dsndxnn  17078  unifndxnn  17088  prdsbasex  17142  prdsds  17156  yonedalem3  17979  isposix  18024  isposixOLD  18025  plusffval  18313  efmnd1hash  18512  efmnd2hash  18514  smndex1bas  18526  smndex1sgrp  18528  smndex1mnd  18530  smndex1id  18531  smndex2dbas  18534  smndex2hbas  18536  grpsubfval  18604  mulgfval  18683  symg1hash  18978  symg2hash  18980  symgvalstruct  18985  symgvalstructOLD  18986  symgfisg  19057  psgnsn  19109  psgnprfval1  19111  odfval  19121  sylow2alem2  19204  efgsval2  19320  efgsp1  19324  pgpfaclem1  19665  dvdsrval  19868  isirred  19922  scaffval  20122  xrsex  20594  zlmlemOLD  20700  znle  20721  znidomb  20750  cnmsgnsubg  20763  refld  20805  ipffval  20834  psrbag0  21251  psrbagsn  21252  psr1baslem  21337  mat1dimbas  21602  mat1dimscm  21605  mat1f1o  21608  mat1rhmelval  21610  m2detleib  21761  pmatcoe1fsupp  21831  indistopon  22132  iccordt  22346  conncompid  22563  ptbasfi  22713  ptcmpfi  22945  ustfn  23334  ust0  23352  ustn0  23353  tmslem  23618  tmslemOLD  23619  nmfval  23725  tnglemOLD  23778  cnbl0  23918  cnopn  23931  remet  23934  re2ndc  23945  zcld  23957  icccmp  23969  xrge0gsumle  23977  xrge0tsms  23978  xmetdcn  23982  divcn  24012  expcn  24016  iiconn  24031  idcncf  24062  cnmpopc  24072  cnrehmeo  24097  cnheiborlem  24098  rellycmp  24101  bndth  24102  evth2  24104  cnrlmod  24287  cnrlvec  24288  cncmet  24467  ishl2  24515  ehleudis  24563  ehleudisval  24564  finiunmbl  24689  ioombl1lem4  24706  vitalilem4  24756  vitalilem5  24757  ismbf2d  24785  mbfimaopnlem  24800  mbfi1fseqlem6  24866  itgex  24916  bddmulibl  24984  ditgex  24997  recnperf  25050  dvcnvrelem2  25163  ftc1  25187  mdegcl  25215  plyeq0lem  25352  aaliou3lem4  25487  dvradcnv  25561  sincn  25584  coscn  25585  tanabsge  25644  circsubm  25690  reloggim  25735  logcn  25783  dvloglem  25784  logdmopn  25785  dvlog2  25789  2irrexpq  25866  cxpcn  25879  cxpcn3  25882  resqrtcn  25883  2logb9irrALT  25929  2irrexpqALT  25931  atanrecl  26042  atan1  26059  atansopn  26063  birthdaylem1  26082  birthday  26085  emcllem4  26129  emcllem6  26131  lgamgulmlem6  26164  basellem6  26216  ppiublem1  26331  bposlem6  26418  bposlem8  26420  lgslem4  26429  lgsdir2lem2  26455  selberglem1  26674  selberglem3  26676  selberg  26677  selbergs  26703  qdrng  26749  edgfndxnn  27341  structvtxvallem  27371  usgrexmpllem  27608  usgrexmpl  27611  uhgrspan1  27651  upgrres  27654  umgrres  27655  usgrres  27656  upgrres1  27661  umgrres1  27662  usgrres1  27663  fusgrfis  27678  cusgrres  27796  vtxdlfgrval  27833  vtxdusgr0edgnelALT  27844  umgr2v2e  27873  vtxdginducedm1lem1  27887  vtxdginducedm1fi  27892  finsumvtxdg2ssteplem4  27896  pthdlem1  28113  crctcshlem3  28163  2wlkd  28280  2wlkond  28281  2trlond  28283  2pthd  28284  2pthond  28286  umgr2adedgwlkonALT  28291  0pth  28468  wlk2v2e  28500  3wlkd  28513  3trlond  28516  3pthd  28517  3pthond  28518  3spthond  28520  eupthvdres  28578  eulerpathpr  28583  konigsbergumgr  28594  konigsberglem5  28599  konigsberg  28600  ex-lcm  28801  isvciOLD  28921  isnvi  28954  blocni  29146  hmoval  29151  cncph  29160  ipasslem7  29177  siilem2  29193  normlem2  29452  normlem3  29453  normlem6  29456  h0elch  29596  hhssabloilem  29602  hhsssh  29610  spansnji  29987  nonbooli  29992  3oalem5  30007  3oalem6  30008  3oai  30009  mayetes3i  30070  nmcexi  30367  nmbdfnlb  30391  rnelshi  30400  cnlnadjlem5  30412  pjbdlni  30490  golem2  30613  goeqi  30614  dp2clq  31134  rpdp2cl  31135  rpdp2cl2  31136  dpmul100  31150  rpdpcl  31156  xrge0tsmsd  31296  pmtrto1cl  31345  psgnfzto1stlem  31346  fzto1st  31349  psgnfzto1st  31351  nn0omnd  31524  xrge0slmod  31527  qusima  31573  prmidl0  31605  fply1  31646  ccfldextdgrr  31721  circtopn  31766  circcn  31767  zarcmplem  31810  tpr2tp  31833  tpr2rico  31841  ordtprsval  31847  ordtprsuni  31848  ordtrestNEW  31850  ordtrest2NEWlem  31851  ordtrest2NEW  31852  ordtconnlem1  31853  mndpluscn  31855  xrge0pluscn  31869  xrge0mulc1cn  31870  xrge0haus  31873  lmlimxrge0  31877  lmxrge0  31881  qqhcn  31920  qqhucn  31921  esumex  31976  esumcst  32010  hasheuni  32032  esumcvg  32033  prsiga  32078  brsiga  32130  mbfmcnt  32214  sxbrsigalem3  32218  dya2iocuni  32229  dya2iocucvr  32230  sxbrsigalem1  32231  sxbrsiga  32236  eulerpartlemt  32317  fibp1  32347  coinflipprob  32425  coinfliprv  32428  ccatmulgnn0dir  32500  signswplusg  32513  hgt750lem2  32611  hgt750leme  32617  bnj105  32682  bnj918  32725  bnj95  32823  bnj852  32880  bnj865  32882  subfacp1lem1  33120  subfacp1lem3  33123  subfacp1lem5  33125  subfacp1lem6  33126  kur14lem7  33153  iisconn  33193  iillysconn  33194  cvmliftlem5  33230  cvmliftlem8  33233  cvmliftlem10  33235  cvmlift2lem9  33252  satfv0  33299  goalrlem  33337  goalr  33338  satffunlem2lem2  33347  circum  33611  iexpire  33680  0sno  33999  1sno  34000  lrrecse  34078  altopex  34241  colinearex  34341  ssoninhaus  34616  cnndvlem2  34697  bj-pinftyccb  35371  taupi  35473  isbasisrelowl  35508  relowlpssretop  35514  poimirlem29  35785  poimirlem30  35786  poimirlem31  35787  dvasin  35840  dvacos  35841  areacirc  35849  upixp  35866  fdc  35882  lmclim2  35895  cncfres  35902  heibor1lem  35946  rrnval  35964  rrnmet  35966  reheibor  35976  isdrngo2  36095  isrngohom  36102  idlval  36150  isidl  36151  igenval  36198  scottexf  36305  cnvepresex  36448  renegclALT  36956  ldualfvadd  37121  cmtfvalN  37203  cvrfval  37261  cdleme31fv  38383  cdlemk40  38910  cdlemk56  38964  dibopelvalN  39136  dibopelval2  39138  dibelval3  39140  diblsmopel  39164  cdlemn11a  39200  dihopelvalcpre  39241  dihpN  39329  hlhilsca  39928  hlhilip  39945  3factsumint1  40009  lcmineqlem23  40039  aks4d1p1p6  40061  aks4d1p1p5  40063  acos1half  40150  sn-0tie0  40401  itrere  40416  retire  40417  prjspval  40422  flt4lem5e  40473  mapfzcons2  40521  jm2.23  40798  jm2.27dlem2  40812  jm2.27dlem4  40814  rmydioph  40816  rmxdioph  40818  expdiophlem2  40824  expdioph  40825  aomclem6  40864  pwslnmlem0  40896  frlmpwfi  40903  mncn0  40944  aaitgo  40967  arearect  41026  areaquad  41027  comptiunov2i  41267  frege110  41534  frege133  41557  scottex2  41816  radcnvrat  41885  uzmptshftfval  41917  dvradcnv2  41918  binomcxplemdvbinom  41924  binomcxplemcvg  41925  binomcxplemnotnn0  41927  rfcnpre1  42515  fcnre  42521  refsumcn  42526  refsum2cnlem1  42533  unirnmapsn  42707  infxrpnf  42940  iocopn  43012  icoopn  43017  mccl  43093  clim1fr1  43096  islptre  43114  sumnnodd  43125  lptre2pt  43135  limclner  43146  limclr  43150  expfac  43152  0cnf  43372  icccncfext  43382  ioodvbdlimc1lem2  43427  ioodvbdlimc2lem  43429  itgsin0pilem1  43445  iblempty  43460  itgvol0  43463  stoweidlem47  43542  stoweidlem53  43548  stoweidlem57  43552  stoweidlem59  43554  wallispilem3  43562  wallispilem4  43563  wallispilem5  43564  wallispi  43565  stirlinglem1  43569  stirlinglem8  43576  stirlinglem12  43580  stirlinglem13  43581  stirlinglem14  43582  stirlinglem15  43583  dirkerper  43591  dirkercncflem2  43599  fourierdlem16  43618  fourierdlem21  43623  fourierdlem22  43624  fourierdlem36  43638  fourierdlem42  43644  fourierdlem71  43672  fourierdlem83  43684  fourierdlem102  43703  fourierdlem103  43704  fourierdlem104  43705  fourierdlem111  43712  fourierdlem112  43713  fourierdlem114  43715  sqwvfoura  43723  sqwvfourb  43724  fourierswlem  43725  fouriersw  43726  etransclem48  43777  salexct3  43835  salgencntex  43836  salgensscntex  43837  iooborel  43844  bor1sal  43848  gsumge0cl  43863  sge0tsms  43872  sge0isum  43919  nnfoctbdjlem  43947  isomenndlem  44022  mbfresmf  44226  incsmflem  44228  incsmf  44229  smfmbfcex  44246  decsmflem  44252  decsmf  44253  smflimlem1  44257  smfpimbor1lem2  44284  smf2id  44286  smfco  44287  smfpimcclem  44291  sprsymrelfolem1  44896  sprbisymrel  44903  fmtno0prm  44962  fmtno1prm  44963  fmtno2prm  44964  fmtno3prm  44966  fmtno4prm  44979  m2prm  44995  m3prm  44996  m5prm  45002  m7prm  45004  lighneallem4a  45012  0evenALTV  45092  1oddALTV  45094  2evenALTV  45096  6even  45115  7odd  45116  8even  45117  9gbo  45178  strisomgrop  45244  ushrisomgr  45245  uspgrex  45264  issubmgm2  45296  lmod1zrnlvec  45787  zlmodzxzldeplem1  45793  zlmodzxzldeplem3  45795  zlmodzxzldeplem4  45796  zlmodzxzldep  45797  ldepsnlinclem1  45798  ldepsnlinclem2  45799  blennn0elnn  45875  nn0sumshdiglemA  45917  nn0sumshdiglemB  45918  itcovalpclem2  45969  itcovalt2lem2  45974  ackval42  45994  rrx2line  46038  rrx2linesl  46041  spheres  46044  2sphere  46047  2sphere0  46048  line2x  46052  line2y  46053  functhinclem1  46274  prsthinc  46287