Theorem eqeltri 2827

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

Syntax hints:   = wceq 1541   ∈ wcel 2111

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  eqeltrri  2828  3eltr4i  2844  intab  4926  axrep6g  5226  unisn2  5248  inex2  5254  vpwex  5313  ord3ex  5323  zfpair  5357  vsnex  5370  opex  5402  otex  5403  uniopel  5454  elvvuni  5691  isarep2  6571  fvex  6835  fvexi  6836  riotaex  7307  ovexi  7380  tpex  7679  oprabex  7908  oprabrexex2  7910  mpoexw  8010  mptmpoopabbrd  8012  mptmpoopabbrdOLD  8013  tfrlem16  8312  1oex  8395  2oex  8396  1on  8397  2on  8398  3on  8401  4on  8402  oesuclem  8440  oecl  8452  o2p2e4  8456  nnecl  8528  1onnALT  8556  2onnALT  8558  3onn  8559  4onn  8560  mapsnf1o2  8818  sbthlem10  9009  cnvfi  9085  fnfi  9087  nnunifi  9175  imafiOLD  9200  pwfi  9203  prfiALT  9209  tpfi  9210  fczfsuppd  9270  cantnfvalf  9555  oemapwe  9584  cantnffval2  9585  cnfcom3clem  9595  ssttrcl  9605  r1fin  9666  hta  9790  infxpenlem  9904  alephon  9960  alephfplem1  9995  dfac5lem4  10017  dfac5lem5  10018  dfac5lem4OLD  10019  kmlem10  10051  fin1a2lem10  10300  fin1a2lem12  10302  hsmexlem9  10316  axcc2lem  10327  domtriomlem  10333  axdc2lem  10339  axcclem  10348  brdom7disj  10422  brdom6disj  10423  iundom2g  10431  konigthlem  10459  canthwelem  10541  wunex2  10629  wunex3  10632  1nq  10819  1pr  10906  nrex1  10955  axcnex  11038  ax1cn  11040  pnfex  11165  mnfxr  11169  cju  12121  nnexALT  12127  2nn  12198  2re  12199  2cn  12200  3nn  12204  3re  12205  3cn  12206  4nn  12208  4re  12209  4cn  12210  5nn  12211  5re  12212  5cn  12213  6nn  12214  6re  12215  6cn  12216  7nn  12217  7re  12218  7cn  12219  8nn  12220  8re  12221  8cn  12222  9nn  12223  9re  12224  9cn  12225  nn0ex  12387  zexALT  12488  nneo  12557  zeo  12559  deccl  12603  10re  12607  decnncl  12608  numnncl2  12611  decnncl2  12612  numsucc  12628  numma2c  12634  numadd  12635  numaddc  12636  nummul1c  12637  nummul2c  12638  decmul1  12652  qexALT  12862  xrex  12885  xnegex  13107  xnegcl  13112  ixxssxr  13257  fz0to4untppr  13530  fz0to5un2tp  13531  om2uzuzi  13856  ltweuz  13868  axdc4uzlem  13890  seqex  13910  seqexw  13924  m1expcl2  13992  faccl  14190  facwordi  14196  faclbnd2  14198  bccl  14229  hashen1  14277  hashrabrsn  14279  hashunlei  14332  hashpw  14343  tpf1o  14408  s1cli  14513  ccat2s1p1  14537  cats1un  14628  revs1  14672  cshwsexa  14731  cats1cli  14764  cats1fvn  14765  crre  15021  remim  15024  climmpt  15478  sumex  15595  supcvg  15763  geo2lim  15782  prodex  15812  bpoly4  15966  ere  15996  eftlub  16018  efsep  16019  tan0  16060  ef01bndlem  16093  nn0o  16294  divalglem5  16308  divalglem9  16312  sadcf  16364  smupf  16389  crth  16689  phimullem  16690  pczpre  16759  pockthi  16819  prmreclem2  16829  igz  16846  0ramcl  16935  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  1259prm  17047  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  4001prm  17056  strle1  17069  ndxarg  17107  basendxnn  17130  plusgndxnn  17189  tsetndxnn  17258  plendxnn  17272  dsndxnn  17291  unifndxnn  17301  prdsbasex  17354  prdsds  17368  yonedalem3  18186  isposix  18230  chnub  18528  plusffval  18554  issubmgm2  18611  efmnd1hash  18800  efmnd2hash  18802  smndex1bas  18814  smndex1sgrp  18816  smndex1mnd  18818  smndex1id  18819  smndex2dbas  18822  smndex2hbas  18824  grpsubfval  18896  mulgfval  18982  symg1hash  19302  symg2hash  19304  symgvalstruct  19309  symgfisg  19380  psgnsn  19432  psgnprfval1  19434  odfval  19444  sylow2alem2  19530  efgsval2  19645  efgsp1  19649  pgpfaclem1  19995  dvdsrval  20279  isirred  20337  scaffval  20813  cnfldex  21294  xrsex  21321  pzriprnglem4  21421  pzriprnglem5  21422  pzriprnglem6  21423  pzriprng1ALT  21433  znle  21473  znidomb  21498  cnmsgnsubg  21514  refld  21556  ipffval  21585  psrbag0  21997  psrbagsn  21998  psr1baslem  22097  mat1dimbas  22387  mat1dimscm  22390  mat1f1o  22393  mat1rhmelval  22395  m2detleib  22546  pmatcoe1fsupp  22616  indistopon  22916  iccordt  23129  conncompid  23346  ptbasfi  23496  ptcmpfi  23728  ustfn  24117  ust0  24135  ustn0  24136  tmslem  24397  nmfval  24503  cnbl0  24688  cnopn  24701  remet  24705  re2ndc  24716  zcld  24729  icccmp  24741  xrge0gsumle  24749  xrge0tsms  24750  xmetdcn  24754  divcnOLD  24784  divcn  24786  expcn  24790  expcnOLD  24792  iiconn  24807  idcncf  24838  cnmpopc  24849  cnrehmeo  24878  cnrehmeoOLD  24879  cnheiborlem  24880  rellycmp  24883  bndth  24884  evth2  24886  cnrlmod  25070  cnrlvec  25071  cncmet  25249  ishl2  25297  ehleudis  25345  ehleudisval  25346  finiunmbl  25472  ioombl1lem4  25489  vitalilem4  25539  vitalilem5  25540  ismbf2d  25568  mbfimaopnlem  25583  mbfi1fseqlem6  25648  itgex  25698  bddmulibl  25767  ditgex  25780  recnperf  25833  dvcnvrelem2  25950  ftc1  25976  mdegcl  26001  plyeq0lem  26142  aaliou3lem4  26281  dvradcnv  26357  sincn  26381  coscn  26382  tanabsge  26442  circsubm  26489  reloggim  26535  logcn  26583  dvloglem  26584  logdmopn  26585  dvlog2  26589  2irrexpq  26667  cxpcn  26681  cxpcnOLD  26682  cxpcn3  26685  resqrtcn  26686  2logb9irrALT  26735  2irrexpqALT  26737  atanrecl  26848  atan1  26865  atansopn  26869  birthdaylem1  26888  birthday  26891  emcllem4  26936  emcllem6  26938  lgamgulmlem6  26971  basellem6  27023  ppiublem1  27140  bposlem6  27227  bposlem8  27229  lgslem4  27238  lgsdir2lem2  27264  selberglem1  27483  selberglem3  27485  selberg  27486  selbergs  27512  qdrng  27558  0sno  27770  1sno  27771  lrrecse  27885  precsexlem11  28155  seqsex  28215  nnsex  28247  n0sbday  28280  n0subs  28289  n0p1nns  28296  dfnns2  28297  zsex  28304  zs12ex  28384  zs12half  28390  edgfndxnn  28970  structvtxvallem  28998  usgrexmpllem  29238  usgrexmpl  29241  uhgrspan1  29281  upgrres  29284  umgrres  29285  usgrres  29286  upgrres1  29291  umgrres1  29292  usgrres1  29293  fusgrfis  29308  cusgrres  29427  vtxdlfgrval  29464  vtxdusgr0edgnelALT  29475  umgr2v2e  29504  vtxdginducedm1lem1  29518  vtxdginducedm1fi  29523  finsumvtxdg2ssteplem4  29527  pthdlem1  29744  crctcshlem3  29797  2wlkd  29914  2wlkond  29915  2trlond  29917  2pthd  29918  2pthond  29920  umgr2adedgwlkonALT  29925  0pth  30105  wlk2v2e  30137  3wlkd  30150  3trlond  30153  3pthd  30154  3pthond  30155  3spthond  30157  eupthvdres  30215  eulerpathpr  30220  konigsbergumgr  30231  konigsberglem5  30236  konigsberg  30237  ex-lcm  30438  isvciOLD  30560  isnvi  30593  blocni  30785  hmoval  30790  cncph  30799  ipasslem7  30816  siilem2  30832  normlem2  31091  normlem3  31092  normlem6  31095  h0elch  31235  hhssabloilem  31241  hhsssh  31249  spansnji  31626  nonbooli  31631  3oalem5  31646  3oalem6  31647  3oai  31648  mayetes3i  31709  nmcexi  32006  nmbdfnlb  32030  rnelshi  32039  cnlnadjlem5  32051  pjbdlni  32129  golem2  32252  goeqi  32253  dp2clq  32861  rpdp2cl  32862  rpdp2cl2  32863  dpmul100  32877  rpdpcl  32883  xrge0tsmsd  33042  pmtrto1cl  33068  psgnfzto1stlem  33069  fzto1st  33072  psgnfzto1st  33074  nn0omnd  33309  xrge0slmod  33313  qusima  33373  prmidl0  33415  fply1  33521  ply1degltdimlem  33635  ccfldextdgrr  33685  algextdeglem8  33737  constrfin  33759  2sqr3minply  33793  2sqr3nconstr  33794  cos9thpiminplylem4  33798  cos9thpiminplylem5  33799  cos9thpinconstrlem2  33803  circtopn  33850  circcn  33851  zarcmplem  33894  tpr2tp  33917  tpr2rico  33925  ordtprsval  33931  ordtprsuni  33932  ordtrestNEW  33934  ordtrest2NEWlem  33935  ordtrest2NEW  33936  ordtconnlem1  33937  mndpluscn  33939  xrge0pluscn  33953  xrge0mulc1cn  33954  xrge0haus  33957  lmlimxrge0  33961  lmxrge0  33965  qqhcn  34004  qqhucn  34005  esumex  34042  esumcst  34076  hasheuni  34098  esumcvg  34099  prsiga  34144  brsiga  34196  mbfmcnt  34281  sxbrsigalem3  34285  dya2iocuni  34296  dya2iocucvr  34297  sxbrsigalem1  34298  sxbrsiga  34303  eulerpartlemt  34384  fibp1  34414  coinflipprob  34493  coinfliprv  34496  ccatmulgnn0dir  34555  signswplusg  34568  hgt750lem2  34665  hgt750leme  34671  bnj105  34736  bnj918  34778  bnj95  34876  bnj852  34933  bnj865  34935  fineqvnttrclse  35144  subfacp1lem1  35223  subfacp1lem3  35226  subfacp1lem5  35228  subfacp1lem6  35229  kur14lem7  35256  iisconn  35296  iillysconn  35297  cvmliftlem5  35333  cvmliftlem8  35336  cvmliftlem10  35338  cvmlift2lem9  35355  satfv0  35402  goalrlem  35440  goalr  35441  satffunlem2lem2  35450  circum  35718  iexpire  35779  altopex  36002  colinearex  36102  ssoninhaus  36490  cnndvlem2  36580  bj-prex  37082  bj-prfromadj  37087  bj-pinftyccb  37263  taupi  37365  isbasisrelowl  37400  relowlpssretop  37406  poimirlem29  37697  poimirlem30  37698  poimirlem31  37699  dvasin  37752  dvacos  37753  areacirc  37761  upixp  37777  fdc  37793  lmclim2  37806  cncfres  37813  heibor1lem  37857  rrnval  37875  rrnmet  37877  reheibor  37887  isdrngo2  38006  isrngohom  38013  idlval  38061  isidl  38062  igenval  38109  scottexf  38216  cnvepresex  38372  renegclALT  39010  ldualfvadd  39175  cmtfvalN  39257  cvrfval  39315  cdleme31fv  40437  cdlemk40  40964  cdlemk56  41018  dibopelvalN  41190  dibopelval2  41192  dibelval3  41194  diblsmopel  41218  cdlemn11a  41254  dihopelvalcpre  41295  dihpN  41383  hlhilsca  41982  hlhilip  41995  3factsumint1  42062  lcmineqlem23  42092  aks4d1p1p6  42114  aks4d1p1p5  42116  aks6d1c6isolem2  42216  itrere  42359  acos1half  42399  redvmptabs  42401  readvrec2  42402  sn-0tie0  42492  sn-itrere  42529  sn-retire  42530  prjspval  42644  flt4lem5e  42697  sn-isghm  42714  mapfzcons2  42760  jm2.23  43037  jm2.27dlem2  43051  jm2.27dlem4  43053  rmydioph  43055  rmxdioph  43057  expdiophlem2  43063  expdioph  43064  aomclem6  43100  pwslnmlem0  43132  frlmpwfi  43139  mncn0  43180  aaitgo  43203  arearect  43256  areaquad  43257  omcl3g  43375  comptiunov2i  43747  frege110  44014  frege133  44037  scottex2  44286  radcnvrat  44355  uzmptshftfval  44387  dvradcnv2  44388  binomcxplemdvbinom  44394  binomcxplemcvg  44395  binomcxplemnotnn0  44397  permaxinf2lem  45053  rfcnpre1  45064  fcnre  45070  refsumcn  45075  refsum2cnlem1  45082  unirnmapsn  45259  infxrpnf  45492  iocopn  45568  icoopn  45573  mccl  45646  clim1fr1  45649  islptre  45667  sumnnodd  45678  lptre2pt  45686  limclner  45697  limclr  45701  expfac  45703  0cnf  45923  icccncfext  45933  ioodvbdlimc1lem2  45978  ioodvbdlimc2lem  45980  itgsin0pilem1  45996  iblempty  46011  itgvol0  46014  stoweidlem47  46093  stoweidlem53  46099  stoweidlem57  46103  stoweidlem59  46105  wallispilem3  46113  wallispilem4  46114  wallispilem5  46115  wallispi  46116  stirlinglem1  46120  stirlinglem8  46127  stirlinglem12  46131  stirlinglem13  46132  stirlinglem14  46133  stirlinglem15  46134  dirkerper  46142  dirkercncflem2  46150  fourierdlem16  46169  fourierdlem21  46174  fourierdlem22  46175  fourierdlem36  46189  fourierdlem42  46195  fourierdlem71  46223  fourierdlem83  46235  fourierdlem102  46254  fourierdlem103  46255  fourierdlem104  46256  fourierdlem111  46263  fourierdlem112  46264  fourierdlem114  46266  sqwvfoura  46274  sqwvfourb  46275  fourierswlem  46276  fouriersw  46277  etransclem48  46328  salexct3  46388  salgencntex  46389  salgensscntex  46390  iooborel  46397  bor1sal  46401  gsumge0cl  46417  sge0tsms  46426  sge0isum  46473  nnfoctbdjlem  46501  isomenndlem  46576  mbfresmf  46785  incsmflem  46787  incsmf  46788  smfmbfcex  46806  decsmflem  46812  decsmf  46813  smflimlem1  46817  smfpimbor1lem2  46845  smf2id  46847  smfco  46848  smfpimcclem  46853  lambert0  46926  sprsymrelfolem1  47531  sprbisymrel  47538  fmtno0prm  47597  fmtno1prm  47598  fmtno2prm  47599  fmtno3prm  47601  fmtno4prm  47614  m2prm  47630  m3prm  47631  m5prm  47637  m7prm  47639  lighneallem4a  47647  0evenALTV  47727  1oddALTV  47729  2evenALTV  47731  6even  47750  7odd  47751  8even  47752  9gbo  47813  opstrgric  47965  ushggricedg  47966  grtri  47979  usgrexmpl1  48061  usgrexmpl1vtx  48062  usgrexmpl1edg  48063  usgrexmpl2  48066  usgrexmpl2vtx  48067  usgrexmpl2edg  48068  gpgprismgr4cycllem5  48138  pgnbgreunbgr  48164  pgn4cyclex  48165  uspgrex  48189  lmod1zrnlvec  48534  zlmodzxzldeplem1  48540  zlmodzxzldeplem3  48542  zlmodzxzldeplem4  48543  zlmodzxzldep  48544  ldepsnlinclem1  48545  ldepsnlinclem2  48546  blennn0elnn  48617  nn0sumshdiglemA  48659  nn0sumshdiglemB  48660  itcovalpclem2  48711  itcovalt2lem2  48716  ackval42  48736  rrx2line  48780  rrx2linesl  48783  spheres  48786  2sphere  48789  2sphere0  48790  line2x  48794  line2y  48795  resipos  49014  functhinclem1  49484  prsthinc  49504  setc1oterm  49531  funcsetc1ocl  49536  funcsetc1o  49537  isinito2lem  49538  isinito3  49540  functermc2  49549  incat  49641  setc1onsubc  49642