Theorem eqeltri 2858

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

Syntax hints:   = wceq 1560   ∈ wcel 2142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837

This theorem is referenced by:  eqeltrri  2859  3eltr4i  2875  intab  4936  axrep6g  5240  unisn2  5262  inex2  5274  vpwex  5334  ord3ex  5344  zfpair  5378  vsnex  5392  snex  5396  opex  5431  opexOLD  5432  otex  5433  uniopel  5485  elvvuni  5724  isarep2  6611  fvex  6880  fvexi  6881  riotaex  7357  ovexi  7430  tpex  7729  oprabex  7957  oprabrexex2  7959  mpoexw  8059  mptmpoopabbrd  8062  tfrlem16  8364  1oex  8447  2oex  8449  1on  8450  2on  8451  3on  8454  4on  8455  oesuclem  8494  oecl  8506  o2p2e4  8510  nnecl  8583  1onnALT  8611  2onnALT  8613  3onn  8614  4onn  8615  mapsnf1o2  8876  sbthlem10  9068  cnvfi  9144  fnfi  9146  nnunifi  9235  imafiOLD  9260  pwfi  9263  prfiALT  9269  tpfi  9270  fczfsuppd  9332  cantnfvalf  9620  oemapwe  9649  cantnffval2  9650  cnfcom3clem  9660  ssttrcl  9670  r1fin  9731  hta  9855  infxpenlem  9969  alephon  10025  alephfplem1  10060  dfac5lem4  10082  dfac5lem5  10083  dfac5lem4OLD  10084  kmlem10  10116  fin1a2lem10  10366  fin1a2lem12  10368  hsmexlem9  10382  axcc2lem  10393  domtriomlem  10399  axdc2lem  10405  axcclem  10414  brdom7disj  10488  brdom6disj  10489  iundom2g  10497  konigthlem  10526  canthwelem  10608  wunex2  10696  wunex3  10699  1nq  10886  1pr  10973  nrex1  11022  axcnex  11105  ax1cn  11107  pnfex  11235  mnfxr  11239  cju  12191  nnexALT  12212  2nn  12291  2re  12292  2cn  12293  3nn  12297  3re  12298  3cn  12299  4nn  12301  4re  12302  4cn  12303  5nn  12304  5re  12305  5cn  12306  6nn  12307  6re  12308  6cn  12309  7nn  12310  7re  12311  7cn  12312  8nn  12313  8re  12314  8cn  12315  9nn  12316  9re  12317  9cn  12318  nn0ex  12487  zexALT  12588  nneo  12657  zeo  12659  deccl  12703  10re  12711  decnncl  12712  numnncl2  12716  decnncl2  12717  numsucc  12733  numma2c  12739  numadd  12740  numaddc  12741  nummul1c  12742  nummul2c  12743  decmul1  12757  qexALT  12965  xrex  12988  xnegex  13211  xnegcl  13216  ixxssxr  13361  fz0to4untppr  13635  fz0to5un2tp  13636  om2uzuzi  13962  ltweuz  13974  axdc4uzlem  13996  seqex  14016  seqexw  14030  m1expcl2  14098  faccl  14296  facwordi  14302  faclbnd2  14304  bccl  14335  hashen1  14383  hashrabrsn  14385  hashunlei  14438  hashpw  14449  tpf1o  14514  s1cli  14619  ccat2s1p1  14643  cats1un  14734  revs1  14778  cshwsexa  14837  cats1cli  14870  cats1fvn  14871  crre  15141  remim  15144  climmpt  15598  sumex  15715  supcvg  15886  geo2lim  15905  prodex  15935  bpoly4  16089  ere  16119  eftlub  16141  efsep  16142  tan0  16183  ef01bndlem  16216  nn0o  16417  divalglem5  16431  divalglem9  16435  sadcf  16487  smupf  16512  crth  16813  phimullem  16814  pczpre  16883  pockthi  16943  prmreclem2  16953  igz  16970  0ramcl  17059  1259lem1  17167  1259lem2  17168  1259lem3  17169  1259lem4  17170  1259lem5  17171  1259prm  17172  2503lem1  17173  2503lem2  17174  2503lem3  17175  2503prm  17176  4001lem1  17177  4001lem2  17178  4001lem3  17179  4001lem4  17180  4001prm  17181  strle1  17194  ndxarg  17232  basendxnn  17255  plusgndxnn  17314  tsetndxnn  17383  plendxnn  17397  dsndxnn  17416  unifndxnn  17426  prdsbasex  17479  prdsds  17493  yonedalem3  18312  isposix  18356  chnub  18654  plusffval  18680  issubmgm2  18737  efmnd1hash  18926  efmnd2hash  18928  smndex1bas  18943  smndex1sgrp  18945  smndex1mnd  18947  smndex1id  18948  smndex2dbas  18951  smndex2hbas  18953  grpsubfval  19025  mulgfval  19111  symg1hash  19430  symg2hash  19432  symgvalstruct  19437  symgfisg  19508  psgnsn  19560  psgnprfval1  19562  odfval  19572  sylow2alem2  19658  efgsval2  19773  efgsp1  19777  pgpfaclem1  20123  dvdsrval  20406  isirred  20464  scaffval  20944  cnfldex  21424  xrsex  21438  pzriprnglem4  21533  pzriprnglem5  21534  pzriprnglem6  21535  pzriprng1ALT  21545  znle  21585  znidomb  21610  cnmsgnsubg  21626  refld  21668  ipffval  21697  psrbag0  22112  psrbagsn  22113  psr1baslem  22244  mat1dimbas  22529  mat1dimscm  22532  mat1f1o  22535  mat1rhmelval  22537  m2detleib  22688  pmatcoe1fsupp  22758  indistopon  23058  iccordt  23271  conncompid  23488  ptbasfi  23638  ptcmpfi  23870  ustfn  24259  ust0  24277  ustn0  24278  tmslem  24539  nmfval  24645  cnbl0  24830  cnopn  24843  remet  24847  re2ndc  24858  zcld  24871  icccmp  24883  xrge0gsumle  24891  xrge0tsms  24892  xmetdcn  24896  divcn  24927  expcn  24931  iiconn  24946  idcncf  24977  cnmpopc  24987  cnrehmeo  25012  cnheiborlem  25013  rellycmp  25016  bndth  25017  evth2  25019  cnrlmod  25202  cnrlvec  25203  cncmet  25381  ishl2  25429  ehleudis  25477  ehleudisval  25478  finiunmbl  25603  ioombl1lem4  25620  vitalilem4  25670  vitalilem5  25671  ismbf2d  25699  mbfimaopnlem  25714  mbfi1fseqlem6  25779  itgex  25829  bddmulibl  25898  ditgex  25911  recnperf  25964  dvcnvrelem2  26077  ftc1  26101  mdegcl  26126  plyeq0lem  26267  aaliou3lem4  26407  dvradcnv  26481  sincn  26504  coscn  26505  tanabsge  26568  circsubm  26615  reloggim  26661  logcn  26709  dvloglem  26710  logdmopn  26711  dvlog2  26715  2irrexpq  26793  cxpcn  26807  cxpcn3  26810  resqrtcn  26811  2logb9irrALT  26860  2irrexpqALT  26862  atanrecl  26973  atan1  26990  atansopn  26994  birthdaylem1  27013  birthday  27016  emcllem4  27060  emcllem6  27062  lgamgulmlem6  27095  basellem6  27147  ppiublem1  27263  bposlem6  27350  bposlem8  27352  lgslem4  27361  lgsdir2lem2  27387  selberglem1  27606  selberglem3  27608  selberg  27609  selbergs  27635  qdrng  27681  0no  27899  1no  27900  lrrecse  28032  precsexlem11  28307  seqsex  28375  nnsex  28408  n0bday  28442  n0subs  28453  n0p1nns  28461  dfnns2  28462  zsex  28470  bdayfinbndlem1  28557  z12sex  28564  z12shalf  28570  edgfndxnn  29190  structvtxvallem  29218  usgrexmpllem  29458  usgrexmpl  29461  uhgrspan1  29501  upgrres  29504  umgrres  29505  usgrres  29506  upgrres1  29511  umgrres1  29512  usgrres1  29513  fusgrfis  29528  cusgrres  29646  vtxdlfgrval  29683  vtxdusgr0edgnelALT  29694  umgr2v2e  29723  vtxdginducedm1lem1  29737  vtxdginducedm1fi  29742  finsumvtxdg2ssteplem4  29746  pthdlem1  29963  crctcshlem3  30016  2wlkd  30133  2wlkond  30134  2trlond  30136  2pthd  30137  2pthond  30139  umgr2adedgwlkonALT  30144  0pth  30324  wlk2v2e  30356  3wlkd  30369  3trlond  30372  3pthd  30373  3pthond  30374  3spthond  30376  eupthvdres  30434  eulerpathpr  30439  konigsbergumgr  30450  konigsberglem5  30455  konigsberg  30456  ex-lcm  30657  isvciOLD  30780  isnvi  30813  blocni  31005  hmoval  31010  cncph  31019  ipasslem7  31036  siilem2  31052  normlem2  31311  normlem3  31312  normlem6  31315  h0elch  31455  hhssabloilem  31461  hhsssh  31469  spansnji  31846  nonbooli  31851  3oalem5  31866  3oalem6  31867  3oai  31868  mayetes3i  31929  nmcexi  32226  nmbdfnlb  32250  rnelshi  32259  cnlnadjlem5  32271  pjbdlni  32349  golem2  32472  goeqi  32473  dp2clq  33055  rpdp2cl  33056  rpdp2cl2  33057  dpmul100  33071  rpdpcl  33077  xrge0tsmsd  33250  pmtrto1cl  33276  psgnfzto1stlem  33277  fzto1st  33280  psgnfzto1st  33282  nn0omnd  33527  xrge0slmod  33531  qusima  33591  prmidl0  33634  fply1  33751  extvfvcl  33830  ply1degltdimlem  33916  ccfldextdgrr  33966  algextdeglem8  34018  constrfin  34040  2sqr3minply  34074  2sqr3nconstr  34075  cos9thpiminplylem4  34079  cos9thpiminplylem5  34080  cos9thpinconstrlem2  34084  circtopn  34131  circcn  34132  zarcmplem  34175  tpr2tp  34198  tpr2rico  34206  ordtprsval  34212  ordtprsuni  34213  ordtrestNEW  34215  ordtrest2NEWlem  34216  ordtrest2NEW  34217  ordtconnlem1  34218  mndpluscn  34220  xrge0pluscn  34234  xrge0mulc1cn  34235  xrge0haus  34238  lmlimxrge0  34242  lmxrge0  34246  qqhcn  34285  qqhucn  34286  esumex  34323  esumcst  34357  hasheuni  34379  esumcvg  34380  prsiga  34425  brsiga  34477  mbfmcnt  34562  sxbrsigalem3  34566  dya2iocuni  34577  dya2iocucvr  34578  sxbrsigalem1  34579  sxbrsiga  34584  eulerpartlemt  34665  fibp1  34695  coinflipprob  34774  coinfliprv  34777  ccatmulgnn0dir  34836  signswplusg  34846  hgt750lem2  34943  hgt750leme  34949  bnj105  35017  bnj918  35059  bnj95  35156  bnj852  35213  bnj865  35215  fineqvnttrclse  35417  subfacp1lem1  35526  subfacp1lem3  35529  subfacp1lem5  35531  subfacp1lem6  35532  kur14lem7  35559  iisconn  35599  iillysconn  35600  cvmliftlem5  35636  cvmliftlem8  35639  cvmliftlem10  35641  cvmlift2lem9  35658  satfv0  35705  goalrlem  35743  goalr  35744  satffunlem2lem2  35753  circum  36021  iexpire  36082  altopex  36307  colinearex  36407  ssoninhaus  36805  cnndvlem2  36973  bj-prex  37522  bj-prfromadj  37527  bj-pinftyccb  37710  taupi  37812  isbasisrelowl  37849  relowlpssretop  37855  poimirlem29  38145  poimirlem30  38146  poimirlem31  38147  dvasin  38200  dvacos  38201  areacirc  38209  upixp  38225  fdc  38241  lmclim2  38254  cncfres  38261  heibor1lem  38305  rrnval  38323  rrnmet  38325  reheibor  38335  isdrngo2  38454  isrngohom  38461  idlval  38509  isidl  38510  igenval  38557  scottexf  38664  cnvepresex  38832  preex  38988  renegclALT  39584  ldualfvadd  39749  cmtfvalN  39831  cvrfval  39889  cdleme31fv  41011  cdlemk40  41538  cdlemk56  41592  dibopelvalN  41764  dibopelval2  41766  dibelval3  41768  diblsmopel  41792  cdlemn11a  41828  dihopelvalcpre  41869  dihpN  41957  hlhilsca  42556  hlhilip  42569  3factsumint1  42635  lcmineqlem23  42665  aks4d1p1p6  42687  aks4d1p1p5  42689  aks6d1c6isolem2  42789  itrere  42924  acos1half  42964  redvmptabs  42966  readvrec2  42967  sn-0tie0  43070  sn-itrere  43107  sn-retire  43108  prjspval  43182  flt4lem5e  43235  sn-isghm  43252  mapfzcons2  43297  jm2.23  43570  jm2.27dlem2  43584  jm2.27dlem4  43586  rmydioph  43588  rmxdioph  43590  expdiophlem2  43596  expdioph  43597  aomclem6  43633  pwslnmlem0  43665  frlmpwfi  43672  mncn0  43713  aaitgo  43736  arearect  43789  areaquad  43790  omcl3g  43908  comptiunov2i  44279  frege110  44546  frege133  44569  scottex2  44818  radcnvrat  44887  uzmptshftfval  44919  dvradcnv2  44920  binomcxplemdvbinom  44926  binomcxplemcvg  44927  binomcxplemnotnn0  44929  permaxinf2lem  45585  rfcnpre1  45596  fcnre  45602  refsumcn  45607  refsum2cnlem1  45614  unirnmapsn  45787  infxrpnf  46017  iocopn  46093  icoopn  46098  mccl  46171  clim1fr1  46174  islptre  46192  sumnnodd  46203  lptre2pt  46211  limclner  46222  limclr  46226  expfac  46228  0cnf  46448  icccncfext  46458  ioodvbdlimc1lem2  46503  ioodvbdlimc2lem  46505  itgsin0pilem1  46521  iblempty  46536  itgvol0  46539  stoweidlem47  46618  stoweidlem53  46624  stoweidlem57  46628  stoweidlem59  46630  wallispilem3  46638  wallispilem4  46639  wallispilem5  46640  wallispi  46641  stirlinglem1  46645  stirlinglem8  46652  stirlinglem12  46656  stirlinglem13  46657  stirlinglem14  46658  stirlinglem15  46659  dirkerper  46667  dirkercncflem2  46675  fourierdlem16  46694  fourierdlem21  46699  fourierdlem22  46700  fourierdlem36  46714  fourierdlem42  46720  fourierdlem71  46748  fourierdlem83  46760  fourierdlem102  46779  fourierdlem103  46780  fourierdlem104  46781  fourierdlem111  46788  fourierdlem112  46789  fourierdlem114  46791  sqwvfoura  46799  sqwvfourb  46800  fourierswlem  46801  fouriersw  46802  etransclem48  46853  salexct3  46913  salgencntex  46914  salgensscntex  46915  iooborel  46922  bor1sal  46926  gsumge0cl  46942  sge0tsms  46951  sge0isum  46998  nnfoctbdjlem  47026  isomenndlem  47101  mbfresmf  47310  incsmflem  47312  incsmf  47313  smfmbfcex  47331  decsmflem  47337  decsmf  47338  smflimlem1  47342  smfpimbor1lem2  47370  smf2id  47372  smfco  47373  smfpimcclem  47378  goldrarr  47472  lambert0  47478  sprsymrelfolem1  48095  sprbisymrel  48102  fmtno0prm  48164  fmtno1prm  48165  fmtno2prm  48166  fmtno3prm  48168  fmtno4prm  48181  m2prm  48197  m3prm  48198  m5prm  48204  m7prm  48206  lighneallem4a  48214  nprmdvdsfacm1lem4  48229  0evenALTV  48307  1oddALTV  48309  2evenALTV  48311  6even  48330  7odd  48331  8even  48332  9gbo  48393  opstrgric  48545  ushggricedg  48546  grtri  48559  usgrexmpl1  48641  usgrexmpl1vtx  48642  usgrexmpl1edg  48643  usgrexmpl2  48646  usgrexmpl2vtx  48647  usgrexmpl2edg  48648  gpgprismgr4cycllem5  48718  pgnbgreunbgr  48744  pgn4cyclex  48745  uspgrex  48769  lmod1zrnlvec  49113  zlmodzxzldeplem1  49119  zlmodzxzldeplem3  49121  zlmodzxzldeplem4  49122  zlmodzxzldep  49123  ldepsnlinclem1  49124  ldepsnlinclem2  49125  blennn0elnn  49196  nn0sumshdiglemA  49238  nn0sumshdiglemB  49239  itcovalpclem2  49290  itcovalt2lem2  49295  ackval42  49315  rrx2line  49359  rrx2linesl  49362  spheres  49365  2sphere  49368  2sphere0  49369  line2x  49373  line2y  49374  resipos  49593  functhinclem1  50062  prsthinc  50082  setc1oterm  50109  funcsetc1ocl  50114  funcsetc1o  50115  isinito2lem  50116  isinito3  50118  functermc2  50127  incat  50219  setc1onsubc  50220