Theorem eqeltri 2833

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 2827	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)
4	1, 3	mpbir 230	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1540   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2728  df-clel 2814

This theorem is referenced by:  eqeltrri  2834  3eltr4i  2850  intab  4921  axrep6g  5231  unisn2  5250  inex2  5256  vpwex  5314  ord3ex  5324  zfpair  5358  opex  5397  otex  5398  uniopel  5448  elvvuni  5681  isarep2  6561  fvex  6824  fvexi  6825  riotaex  7277  ovexi  7350  tpex  7638  oprabex  7865  oprabrexex2  7867  mpoexw  7965  mptmpoopabbrd  7967  tfrlem16  8272  1oex  8355  2oex  8356  1on  8357  1onOLD  8358  2on  8359  2onOLD  8360  3on  8363  4on  8364  2oexOLD  8366  oesuclem  8404  oecl  8416  o2p2e4  8420  nnecl  8493  1onnALT  8520  2onnALT  8522  3onn  8523  4onn  8524  mapsnf1o2  8731  sbthlem10  8935  imafi  9018  pwfi  9021  cnvfi  9023  fnfi  9024  nnunifi  9137  xpfiOLD  9161  prfi  9165  tpfi  9166  pwfiOLD  9190  fczfsuppd  9222  cantnfvalf  9500  oemapwe  9529  cantnffval2  9530  cnfcom3clem  9540  ssttrcl  9550  r1fin  9608  hta  9732  infxpenlem  9848  alephon  9904  alephfplem1  9939  dfac5lem4  9961  dfac5lem5  9962  kmlem10  9994  fin1a2lem10  10244  fin1a2lem12  10246  hsmexlem9  10260  axcc2lem  10271  domtriomlem  10277  axdc2lem  10283  axcclem  10292  brdom7disj  10366  brdom6disj  10367  iundom2g  10375  konigthlem  10403  canthwelem  10485  wunex2  10573  wunex3  10576  1nq  10763  1pr  10850  nrex1  10899  axcnex  10982  ax1cn  10984  pnfex  11107  mnfxr  11111  inelr  12042  cju  12048  nnexALT  12054  2nn  12125  2re  12126  2cn  12127  3nn  12131  3re  12132  3cn  12133  4nn  12135  4re  12136  4cn  12137  5nn  12138  5re  12139  5cn  12140  6nn  12141  6re  12142  6cn  12143  7nn  12144  7re  12145  7cn  12146  8nn  12147  8re  12148  8cn  12149  9nn  12150  9re  12151  9cn  12152  nn0ex  12318  zexALT  12418  nneo  12483  zeo  12485  deccl  12531  10re  12535  decnncl  12536  numnncl2  12539  decnncl2  12540  numsucc  12556  numma2c  12562  numadd  12563  numaddc  12564  nummul1c  12565  nummul2c  12566  decmul1  12580  qexALT  12783  xrex  12806  xnegex  13021  xnegcl  13026  ixxssxr  13170  om2uzuzi  13748  ltweuz  13760  axdc4uzlem  13782  seqex  13802  seqexw  13816  m1expcl2  13883  faccl  14076  facwordi  14082  faclbnd2  14084  bccl  14115  hashen1  14163  hashrabrsn  14165  hashunlei  14218  hashpw  14229  s1cli  14387  ccat2s1p1  14412  cats1un  14510  revs1  14554  cshwsexa  14613  cats1cli  14646  cats1fvn  14647  crre  14901  remim  14904  climmpt  15356  sumex  15475  supcvg  15644  geo2lim  15663  prodex  15693  bpoly4  15845  ere  15874  eftlub  15894  efsep  15895  tan0  15936  ef01bndlem  15969  nn0o  16168  divalglem5  16182  divalglem9  16186  sadcf  16236  smupf  16261  crth  16553  phimullem  16554  pczpre  16622  pockthi  16682  prmreclem2  16692  igz  16709  0ramcl  16798  1259lem1  16906  1259lem2  16907  1259lem3  16908  1259lem4  16909  1259lem5  16910  1259prm  16911  2503lem1  16912  2503lem2  16913  2503lem3  16914  2503prm  16915  4001lem1  16916  4001lem2  16917  4001lem3  16918  4001lem4  16919  4001prm  16920  strle1  16933  ndxarg  16971  basendxnn  16996  basendxnnOLD  16997  plusgndxnn  17064  tsetndxnn  17138  plendxnn  17152  dsndxnn  17171  unifndxnn  17181  prdsbasex  17235  prdsds  17249  yonedalem3  18072  isposix  18117  isposixOLD  18118  plusffval  18406  efmnd1hash  18604  efmnd2hash  18606  smndex1bas  18618  smndex1sgrp  18620  smndex1mnd  18622  smndex1id  18623  smndex2dbas  18626  smndex2hbas  18628  grpsubfval  18696  mulgfval  18775  symg1hash  19070  symg2hash  19072  symgvalstruct  19077  symgvalstructOLD  19078  symgfisg  19149  psgnsn  19201  psgnprfval1  19203  odfval  19213  sylow2alem2  19296  efgsval2  19411  efgsp1  19415  pgpfaclem1  19756  dvdsrval  19959  isirred  20013  scaffval  20221  xrsex  20693  zlmlemOLD  20799  znle  20820  znidomb  20849  cnmsgnsubg  20862  refld  20904  ipffval  20933  psrbag0  21350  psrbagsn  21351  psr1baslem  21436  mat1dimbas  21701  mat1dimscm  21704  mat1f1o  21707  mat1rhmelval  21709  m2detleib  21860  pmatcoe1fsupp  21930  indistopon  22231  iccordt  22445  conncompid  22662  ptbasfi  22812  ptcmpfi  23044  ustfn  23433  ust0  23451  ustn0  23452  tmslem  23717  tmslemOLD  23718  nmfval  23824  tnglemOLD  23877  cnbl0  24017  cnopn  24030  remet  24033  re2ndc  24044  zcld  24056  icccmp  24068  xrge0gsumle  24076  xrge0tsms  24077  xmetdcn  24081  divcn  24111  expcn  24115  iiconn  24130  idcncf  24161  cnmpopc  24171  cnrehmeo  24196  cnheiborlem  24197  rellycmp  24200  bndth  24201  evth2  24203  cnrlmod  24386  cnrlvec  24387  cncmet  24566  ishl2  24614  ehleudis  24662  ehleudisval  24663  finiunmbl  24788  ioombl1lem4  24805  vitalilem4  24855  vitalilem5  24856  ismbf2d  24884  mbfimaopnlem  24899  mbfi1fseqlem6  24965  itgex  25015  bddmulibl  25083  ditgex  25096  recnperf  25149  dvcnvrelem2  25262  ftc1  25286  mdegcl  25314  plyeq0lem  25451  aaliou3lem4  25586  dvradcnv  25660  sincn  25683  coscn  25684  tanabsge  25743  circsubm  25789  reloggim  25834  logcn  25882  dvloglem  25883  logdmopn  25884  dvlog2  25888  2irrexpq  25965  cxpcn  25978  cxpcn3  25981  resqrtcn  25982  2logb9irrALT  26028  2irrexpqALT  26030  atanrecl  26141  atan1  26158  atansopn  26162  birthdaylem1  26181  birthday  26184  emcllem4  26228  emcllem6  26230  lgamgulmlem6  26263  basellem6  26315  ppiublem1  26430  bposlem6  26517  bposlem8  26519  lgslem4  26528  lgsdir2lem2  26554  selberglem1  26773  selberglem3  26775  selberg  26776  selbergs  26802  qdrng  26848  edgfndxnn  27493  structvtxvallem  27523  usgrexmpllem  27760  usgrexmpl  27763  uhgrspan1  27803  upgrres  27806  umgrres  27807  usgrres  27808  upgrres1  27813  umgrres1  27814  usgrres1  27815  fusgrfis  27830  cusgrres  27948  vtxdlfgrval  27985  vtxdusgr0edgnelALT  27996  umgr2v2e  28025  vtxdginducedm1lem1  28039  vtxdginducedm1fi  28044  finsumvtxdg2ssteplem4  28048  pthdlem1  28266  crctcshlem3  28316  2wlkd  28433  2wlkond  28434  2trlond  28436  2pthd  28437  2pthond  28439  umgr2adedgwlkonALT  28444  0pth  28621  wlk2v2e  28653  3wlkd  28666  3trlond  28669  3pthd  28670  3pthond  28671  3spthond  28673  eupthvdres  28731  eulerpathpr  28736  konigsbergumgr  28747  konigsberglem5  28752  konigsberg  28753  ex-lcm  28954  isvciOLD  29074  isnvi  29107  blocni  29299  hmoval  29304  cncph  29313  ipasslem7  29330  siilem2  29346  normlem2  29605  normlem3  29606  normlem6  29609  h0elch  29749  hhssabloilem  29755  hhsssh  29763  spansnji  30140  nonbooli  30145  3oalem5  30160  3oalem6  30161  3oai  30162  mayetes3i  30223  nmcexi  30520  nmbdfnlb  30544  rnelshi  30553  cnlnadjlem5  30565  pjbdlni  30643  golem2  30766  goeqi  30767  dp2clq  31286  rpdp2cl  31287  rpdp2cl2  31288  dpmul100  31302  rpdpcl  31308  xrge0tsmsd  31448  pmtrto1cl  31497  psgnfzto1stlem  31498  fzto1st  31501  psgnfzto1st  31503  nn0omnd  31679  xrge0slmod  31682  qusima  31729  prmidl0  31761  fply1  31802  ccfldextdgrr  31878  circtopn  31923  circcn  31924  zarcmplem  31967  tpr2tp  31990  tpr2rico  31998  ordtprsval  32004  ordtprsuni  32005  ordtrestNEW  32007  ordtrest2NEWlem  32008  ordtrest2NEW  32009  ordtconnlem1  32010  mndpluscn  32012  xrge0pluscn  32026  xrge0mulc1cn  32027  xrge0haus  32030  lmlimxrge0  32034  lmxrge0  32038  qqhcn  32077  qqhucn  32078  esumex  32133  esumcst  32167  hasheuni  32189  esumcvg  32190  prsiga  32235  brsiga  32287  mbfmcnt  32371  sxbrsigalem3  32375  dya2iocuni  32386  dya2iocucvr  32387  sxbrsigalem1  32388  sxbrsiga  32393  eulerpartlemt  32474  fibp1  32504  coinflipprob  32582  coinfliprv  32585  ccatmulgnn0dir  32657  signswplusg  32670  hgt750lem2  32768  hgt750leme  32774  bnj105  32839  bnj918  32881  bnj95  32979  bnj852  33036  bnj865  33038  subfacp1lem1  33276  subfacp1lem3  33279  subfacp1lem5  33281  subfacp1lem6  33282  kur14lem7  33309  iisconn  33349  iillysconn  33350  cvmliftlem5  33386  cvmliftlem8  33389  cvmliftlem10  33391  cvmlift2lem9  33408  satfv0  33455  goalrlem  33493  goalr  33494  satffunlem2lem2  33503  circum  33767  iexpire  33832  0sno  34090  1sno  34091  lrrecse  34169  altopex  34332  colinearex  34432  ssoninhaus  34707  cnndvlem2  34788  bj-prex  35296  bj-pinftyccb  35469  taupi  35571  isbasisrelowl  35606  relowlpssretop  35612  poimirlem29  35883  poimirlem30  35884  poimirlem31  35885  dvasin  35938  dvacos  35939  areacirc  35947  upixp  35964  fdc  35980  lmclim2  35993  cncfres  36000  heibor1lem  36044  rrnval  36062  rrnmet  36064  reheibor  36074  isdrngo2  36193  isrngohom  36200  idlval  36248  isidl  36249  igenval  36296  scottexf  36403  cnvepresex  36572  renegclALT  37202  ldualfvadd  37367  cmtfvalN  37449  cvrfval  37507  cdleme31fv  38630  cdlemk40  39157  cdlemk56  39211  dibopelvalN  39383  dibopelval2  39385  dibelval3  39387  diblsmopel  39411  cdlemn11a  39447  dihopelvalcpre  39488  dihpN  39576  hlhilsca  40175  hlhilip  40192  3factsumint1  40255  lcmineqlem23  40285  aks4d1p1p6  40307  aks4d1p1p5  40309  acos1half  40399  sn-0tie0  40642  itrere  40657  retire  40658  prjspval  40663  flt4lem5e  40714  mapfzcons2  40762  jm2.23  41040  jm2.27dlem2  41054  jm2.27dlem4  41056  rmydioph  41058  rmxdioph  41060  expdiophlem2  41066  expdioph  41067  aomclem6  41106  pwslnmlem0  41138  frlmpwfi  41145  mncn0  41186  aaitgo  41209  arearect  41268  areaquad  41269  comptiunov2i  41553  frege110  41820  frege133  41843  scottex2  42102  radcnvrat  42171  uzmptshftfval  42203  dvradcnv2  42204  binomcxplemdvbinom  42210  binomcxplemcvg  42211  binomcxplemnotnn0  42213  rfcnpre1  42801  fcnre  42807  refsumcn  42812  refsum2cnlem1  42819  unirnmapsn  43000  infxrpnf  43240  iocopn  43313  icoopn  43318  mccl  43394  clim1fr1  43397  islptre  43415  sumnnodd  43426  lptre2pt  43436  limclner  43447  limclr  43451  expfac  43453  0cnf  43673  icccncfext  43683  ioodvbdlimc1lem2  43728  ioodvbdlimc2lem  43730  itgsin0pilem1  43746  iblempty  43761  itgvol0  43764  stoweidlem47  43843  stoweidlem53  43849  stoweidlem57  43853  stoweidlem59  43855  wallispilem3  43863  wallispilem4  43864  wallispilem5  43865  wallispi  43866  stirlinglem1  43870  stirlinglem8  43877  stirlinglem12  43881  stirlinglem13  43882  stirlinglem14  43883  stirlinglem15  43884  dirkerper  43892  dirkercncflem2  43900  fourierdlem16  43919  fourierdlem21  43924  fourierdlem22  43925  fourierdlem36  43939  fourierdlem42  43945  fourierdlem71  43973  fourierdlem83  43985  fourierdlem102  44004  fourierdlem103  44005  fourierdlem104  44006  fourierdlem111  44013  fourierdlem112  44014  fourierdlem114  44016  sqwvfoura  44024  sqwvfourb  44025  fourierswlem  44026  fouriersw  44027  etransclem48  44078  salexct3  44136  salgencntex  44137  salgensscntex  44138  iooborel  44145  bor1sal  44149  gsumge0cl  44165  sge0tsms  44174  sge0isum  44221  nnfoctbdjlem  44249  isomenndlem  44324  mbfresmf  44533  incsmflem  44535  incsmf  44536  smfmbfcex  44554  decsmflem  44560  decsmf  44561  smflimlem1  44565  smfpimbor1lem2  44593  smf2id  44595  smfco  44596  smfpimcclem  44601  sprsymrelfolem1  45214  sprbisymrel  45221  fmtno0prm  45280  fmtno1prm  45281  fmtno2prm  45282  fmtno3prm  45284  fmtno4prm  45297  m2prm  45313  m3prm  45314  m5prm  45320  m7prm  45322  lighneallem4a  45330  0evenALTV  45410  1oddALTV  45412  2evenALTV  45414  6even  45433  7odd  45434  8even  45435  9gbo  45496  strisomgrop  45562  ushrisomgr  45563  uspgrex  45582  issubmgm2  45614  lmod1zrnlvec  46105  zlmodzxzldeplem1  46111  zlmodzxzldeplem3  46113  zlmodzxzldeplem4  46114  zlmodzxzldep  46115  ldepsnlinclem1  46116  ldepsnlinclem2  46117  blennn0elnn  46193  nn0sumshdiglemA  46235  nn0sumshdiglemB  46236  itcovalpclem2  46287  itcovalt2lem2  46292  ackval42  46312  rrx2line  46356  rrx2linesl  46359  spheres  46362  2sphere  46365  2sphere0  46366  line2x  46370  line2y  46371  functhinclem1  46592  prsthinc  46605  tworepnotupword  46791