Theorem eqeltri 2860

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839

This theorem is used by:  eqeltrri  2861  3eltr4i  2877  intab  4943  axrep6g  5249  unisn2  5272  inex2  5285  vpwex  5346  ord3ex  5356  zfpair  5390  vsnex  5400  snex  5404  opex  5439  opexOLD  5440  otex  5441  uniopel  5496  elvvuni  5736  isarep2  6659  fvex  6929  fvexi  6930  riotaex  7412  ovexi  7485  tpex  7794  oprabex  8022  oprabrexex2  8024  mpoexw  8126  mptmpoopabbrd  8129  tfrlem16  8439  1oex  8524  2oex  8526  1on  8527  2on  8528  3on  8531  4on  8532  oesuclem  8571  oecl  8583  o2p2e4  8587  nnecl  8660  1onnALT  8688  2onnALT  8690  3onn  8691  4onn  8692  mapsnf1o2  8960  sbthlem10  9153  cnvfi  9229  fnfi  9231  nnunifi  9321  pwfi  9348  prfiALT  9354  tpfi  9355  fczfsuppd  9415  cantnfvalf  9703  oemapwe  9732  cantnffval2  9733  cnfcom3clem  9743  ssttrcl  9753  r1fin  9817  scottex  9970  scottex2OLD  9983  hta  9999  htaOLD  10000  infxpenlem  10131  alephon  10187  alephfplem1  10222  dfac5lem4  10244  dfac5lem5  10245  kmlem10  10277  fin1a2lem10  10526  fin1a2lem12  10528  hsmexlem9  10542  axcc2lem  10553  domtriomlem  10559  axdc2lem  10565  axcclem  10574  brdom7disj  10649  brdom6disj  10650  iundom2g  10663  konigthlem  10692  canthwelem  10774  wunex2  10862  wunex3  10865  hftsk  10903  1nq  11052  1pr  11139  nrex1  11188  axcnex  11271  ax1cn  11273  pnfex  11401  mnfxr  11405  cju  12356  nnexALT  12377  2nn  12456  2re  12457  2cn  12458  3nn  12462  3re  12463  3cn  12464  4nn  12466  4re  12467  4cn  12468  5nn  12469  5re  12470  5cn  12471  6nn  12472  6re  12473  6cn  12474  7nn  12475  7re  12476  7cn  12477  8nn  12478  8re  12479  8cn  12480  9nn  12481  9re  12482  9cn  12483  nn0ex  12652  zexALT  12753  nneo  12823  zeo  12825  deccl  12869  10re  12877  decnncl  12878  numnncl2  12882  decnncl2  12883  numsucc  12899  numma2c  12905  numadd  12906  numaddc  12907  nummul1c  12908  nummul2c  12909  decmul1  12923  qexALT  13131  xrex  13155  xnegex  13378  xnegcl  13383  ixxssxr  13528  fz0to4untppr  13804  fz0to5un2tp  13805  om2uzuzi  14132  ltweuz  14144  axdc4uzlem  14166  seqex  14186  seqexw  14200  m1expcl2  14268  faccl  14468  facwordi  14474  faclbnd2  14476  bccl  14507  hashen1  14555  hashrabrsn  14557  hashunlei  14611  hashpw  14622  tpf1o  14687  s1cli  14793  ccat2s1p1  14819  cats1un  14912  revs1  14956  cshwsexa  15017  cats1cli  15050  cats1fvn  15051  crre  15324  remim  15327  climmpt  15782  sumex  15899  supcvg  16069  geo2lim  16088  prodex  16118  bpoly4  16269  ere  16299  eftlub  16321  efsep  16322  tan0  16363  ef01bndlem  16396  nn0o  16597  divalglem5  16611  divalglem9  16615  sadcf  16667  smupf  16692  crth  16999  phimullem  17000  pczpre  17069  pockthi  17129  igz  17156  0ramcl  17245  1259lem1  17353  1259lem2  17354  1259lem3  17355  1259lem4  17356  1259lem5  17357  1259prm  17358  2503lem1  17359  2503lem2  17360  2503lem3  17361  2503prm  17362  4001lem1  17363  4001lem2  17364  4001lem3  17365  4001lem4  17366  4001prm  17367  strle1  17380  ndxarg  17418  basendxnn  17441  plusgndxnn  17502  tsetndxnn  17571  plendxnn  17585  dsndxnn  17604  unifndxnn  17614  prdsbasex  17671  prdsds  17685  yonedalem3  18504  isposix  18548  chnub  18846  plusffval  18872  issubmgm2  18942  efmnd1hash  19138  efmnd2hash  19140  smndex1bas  19155  smndex1sgrp  19157  smndex1mnd  19159  smndex1id  19160  smndex2dbas  19163  smndex2hbas  19165  grpsubfval  19244  mulgfval  19329  symg1hash  19655  symg2hash  19657  symgvalstruct  19662  symgfisg  19733  psgnsn  19785  psgnprfval1  19787  odfval  19797  sylow2alem2  19883  efgsval2  19998  efgsp1  20002  pgpfaclem1  20348  dvdsrval  20642  isirred  20700  scaffval  21206  prmidl0  21685  cnfldex  21732  cnfldfunALT  21745  xrsex  21747  pzriprnglem4  21845  pzriprnglem5  21846  pzriprnglem6  21847  pzriprng1ALT  21857  znle  21897  znidomb  21922  cnmsgnsubg  21938  refld  21980  ipffval  22009  psrbag0  22426  psrbagsn  22427  psr1baslem  22558  mat1dimbas  22842  mat1dimscm  22845  mat1f1o  22848  mat1rhmelval  22850  m2detleib  23001  pmatcoe1fsupp  23074  indistopon  23374  iccordt  23587  conncompid  23804  ptbasfi  23955  ptcmpfi  24187  ustfn  24576  ust0  24594  ustn0  24595  tmslem  24856  nmfval  24962  cnbl0  25147  cnopn  25160  remet  25164  re2ndc  25175  zcld  25188  icccmp  25200  xrge0gsumle  25208  xrge0tsms  25209  xmetdcn  25213  divcn  25244  expcn  25248  iiconn  25263  idcncf  25294  cnmpopc  25304  cnrehmeo  25329  cnheiborlem  25330  rellycmp  25333  bndth  25334  evth2  25336  cnrlmod  25519  cnrlvec  25520  cncmet  25698  ishl2  25746  ehleudis  25794  ehleudisval  25795  finiunmbl  25920  ioombl1lem4  25937  vitalilem4  25987  vitalilem5  25988  ismbf2d  26016  mbfimaopnlem  26031  mbfi1fseqlem6  26096  itgex  26146  bddmulibl  26214  ditgex  26227  recnperf  26280  dvcnvrelem2  26393  ftc1  26417  mdegcl  26442  plyeq0lem  26584  iaa  26708  aaliou3lem4  26730  dvradcnv  26805  sincn  26828  coscn  26829  tanabsge  26892  circsubm  26938  reloggim  26984  logcn  27032  dvloglem  27033  logdmopn  27034  dvlog2  27038  2irrexpq  27116  cxpcn  27130  cxpcn3  27133  resqrtcn  27134  2logb9irrALT  27183  2irrexpqALT  27185  atanrecl  27296  atan1  27313  atansopn  27317  birthdaylem1  27336  birthday  27339  emcllem4  27383  emcllem6  27385  lgamgulmlem6  27418  basellem6  27470  ppiublem1  27586  bposlem6  27673  bposlem8  27675  lgslem4  27684  lgsdir2lem2  27710  selberglem1  27929  selberglem3  27931  selberg  27932  selbergs  27958  qdrng  28004  0no  28252  1no  28253  lrrecse  28385  precsexlem11  28660  seqsex  28728  nnsex  28761  n0bday  28795  n0subs  28806  n0p1nns  28814  dfnns2  28815  zsex  28823  bdayfinbndlem1  28910  z12sex  28917  z12shalf  28923  angmgmlem  29452  edgfndxnn  29627  structvtxvallem  29655  usgrexmpllem  29898  usgrexmpl  29901  uhgrspan1  29941  upgrres  29944  umgrres  29945  usgrres  29946  upgrres1  29951  umgrres1  29952  usgrres1  29953  fusgrfis  29968  cusgrres  30086  vtxdlfgrval  30123  vtxdusgr0edgnelALT  30134  umgr2v2e  30163  vtxdginducedm1lem1  30177  vtxdginducedm1fi  30182  finsumvtxdg2ssteplem4  30186  pthdlem1  30409  crctcshlem3  30465  2wlkd  30582  2wlkond  30583  2trlond  30585  2pthd  30586  2pthond  30588  umgr2adedgwlkonALT  30593  0pth  30773  wlk2v2e  30815  3wlkd  30828  3trlond  30831  3pthd  30832  3pthond  30833  3spthond  30835  eupthvdres  30893  eulerpathpr  30898  konigsbergumgr  30909  konigsberglem5  30914  konigsberg  30915  ex-lcm  31116  isvciOLD  31239  isnvi  31272  blocni  31464  hmoval  31469  cncph  31478  ipasslem7  31495  siilem2  31511  normlem2  31770  normlem3  31771  normlem6  31774  h0elch  31914  hhssabloilem  31920  hhsssh  31928  spansnji  32305  nonbooli  32310  3oalem5  32325  3oalem6  32326  3oai  32327  mayetes3i  32388  nmcexi  32685  nmbdfnlb  32709  rnelshi  32718  cnlnadjlem5  32730  pjbdlni  32808  golem2  32931  goeqi  32932  dp2clq  33543  rpdp2cl  33544  rpdp2cl2  33545  dpmul100  33559  rpdpcl  33565  xrge0tsmsd  33733  pmtrto1cl  33759  psgnfzto1stlem  33760  fzto1st  33763  psgnfzto1st  33765  nn0omnd  34009  xrge0slmod  34013  qusima  34063  fply1  34193  extvfvcl  34279  ply1degltdimlem  34365  ccfldextdgrr  34415  algextdeglem8  34467  constrfin  34489  2sqr3minply  34523  2sqr3nconstr  34524  cos9thpiminplylem4  34528  cos9thpiminplylem5  34529  cos9thpinconstrlem2  34533  circtopn  34580  circcn  34581  zarcmplem  34624  tpr2tp  34647  tpr2rico  34655  ordtprsval  34661  ordtprsuni  34662  ordtrestNEW  34664  ordtrest2NEWlem  34665  ordtrest2NEW  34666  ordtconnlem1  34667  mndpluscn  34669  xrge0pluscn  34683  xrge0mulc1cn  34684  xrge0haus  34687  lmlimxrge0  34691  lmxrge0  34695  qqhcn  34734  qqhucn  34735  esumex  34772  esumcst  34806  hasheuni  34828  esumcvg  34829  prsiga  34874  brsiga  34927  mbfmcnt  35011  sxbrsigalem3  35015  dya2iocuni  35026  dya2iocucvr  35027  sxbrsigalem1  35028  sxbrsiga  35033  eulerpartlemt  35114  fibp1  35144  coinflipprob  35223  coinfliprv  35226  ccatmulgnn0dir  35285  signswplusg  35295  hgt750lem2  35392  hgt750leme  35398  bnj105  35466  bnj918  35508  bnj95  35605  bnj852  35662  bnj865  35664  5on  35904  6on  35905  7on  35906  8on  35907  9on  35908  5onn  35909  6onn  35910  7onn  35911  8onn  35912  9onn  35913  fineqvnttrclse  35933  subfacp1lem1  36152  subfacp1lem3  36155  subfacp1lem5  36157  subfacp1lem6  36158  kur14lem7  36185  iisconn  36225  iillysconn  36226  cvmliftlem5  36262  cvmliftlem8  36265  cvmliftlem10  36267  cvmlift2lem9  36284  satfv0  36331  goalrlem  36369  goalr  36370  satffunlem2lem2  36379  circum  36647  iexpire  36715  altopex  36940  colinearex  37040  ssoninhaus  37451  cnndvlem2  37619  bj-prex  38168  bj-prfromadj  38173  bj-pinftyccb  38410  taupi  38512  isbasisrelowl  38549  relowlpssretop  38555  poimirlem29  38835  poimirlem30  38836  poimirlem31  38837  dvasin  38890  dvacos  38891  areacirc  38899  upixp  38931  fdc  38945  lmclim2  38958  cncfres  38965  heibor1lem  39009  rrnval  39027  rrnmet  39029  reheibor  39039  isdrngo2  39158  isrngohom  39165  idlval  39213  isidl  39214  igenval  39261  scottexf  39366  cnvepresex  39534  preex  39690  renegclALT  40286  ldualfvadd  40451  cmtfvalN  40533  cvrfval  40591  cdleme31fv  41713  cdlemk40  42240  cdlemk56  42294  dibopelvalN  42466  dibopelval2  42468  dibelval3  42470  diblsmopel  42494  cdlemn11a  42530  dihopelvalcpre  42571  dihpN  42659  hlhilsca  43258  hlhilip  43271  3factsumint1  43337  lcmineqlem23  43367  aks4d1p1p6  43389  aks4d1p1p5  43391  aks6d1c6isolem2  43491  25or6to4  43522  itrere  43641  acos1half  43675  redvmptabs  43677  readvrec2  43678  sn-0tie0  43781  sn-itrere  43818  sn-retire  43819  prjspval  43897  sn-isghm  43950  mapfzcons2  43996  jm2.23  44269  jm2.27dlem2  44283  jm2.27dlem4  44285  rmydioph  44287  rmxdioph  44289  expdiophlem2  44295  expdioph  44296  aomclem6  44327  pwslnmlem0  44359  frlmpwfi  44366  mncn0  44406  aaitgo  44429  arearect  44478  areaquad  44479  omcl3g  44597  comptiunov2i  44967  frege110  45234  frege133  45257  radcnvrat  45559  uzmptshftfval  45591  dvradcnv2  45592  binomcxplemdvbinom  45598  binomcxplemcvg  45599  binomcxplemnotnn0  45601  permaxinf2lem  46266  rfcnpre1  46310  fcnre  46316  refsumcn  46321  refsum2cnlem1  46328  unirnmapsn  46500  infxrpnf  46729  iocopn  46805  icoopn  46810  mccl  46883  clim1fr1  46886  islptre  46904  sumnnodd  46915  lptre2pt  46923  limclner  46934  limclr  46938  expfac  46940  0cnf  47160  icccncfext  47170  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  itgsin0pilem1  47233  iblempty  47248  itgvol0  47251  stoweidlem47  47330  stoweidlem53  47336  stoweidlem57  47340  stoweidlem59  47342  wallispilem3  47350  wallispilem4  47351  wallispilem5  47352  wallispi  47353  stirlinglem1  47357  stirlinglem8  47364  stirlinglem12  47368  stirlinglem13  47369  stirlinglem14  47370  stirlinglem15  47371  dirkerper  47379  dirkercncflem2  47387  fourierdlem16  47406  fourierdlem21  47411  fourierdlem22  47412  fourierdlem36  47426  fourierdlem42  47432  fourierdlem71  47460  fourierdlem83  47472  fourierdlem102  47491  fourierdlem103  47492  fourierdlem104  47493  fourierdlem111  47500  fourierdlem112  47501  fourierdlem114  47503  sqwvfoura  47511  sqwvfourb  47512  fourierswlem  47513  fouriersw  47514  etransclem48  47565  salexct3  47625  salgencntex  47626  salgensscntex  47627  iooborel  47634  bor1sal  47638  gsumge0cl  47654  sge0tsms  47663  sge0isum  47710  nnfoctbdjlem  47738  isomenndlem  47813  mbfresmf  48022  incsmflem  48024  incsmf  48025  smfmbfcex  48043  decsmflem  48049  decsmf  48050  smflimlem1  48054  smfpimbor1lem2  48082  smf2id  48084  smfco  48085  smfpimcclem  48090  goldrarr  48201  lambert0  48210  tannpoly  48213  sprsymrelfolem1  48847  sprbisymrel  48854  fmtno0prm  48916  fmtno1prm  48917  fmtno2prm  48918  fmtno3prm  48920  fmtno4prm  48933  m2prm  48949  m3prm  48950  m5prm  48956  m7prm  48958  lighneallem4a  48966  nprmdvdsfacm1lem4  48981  0evenALTV  49059  1oddALTV  49061  2evenALTV  49063  6even  49082  7odd  49083  8even  49084  9gbo  49145  opstrgric  49297  ushggricedg  49298  grtri  49311  usgrexmpl1  49393  usgrexmpl1vtx  49394  usgrexmpl1edg  49395  usgrexmpl2  49398  usgrexmpl2vtx  49399  usgrexmpl2edg  49400  gpgprismgr4cycllem5  49470  pgnbgreunbgr  49496  pgn4cyclex  49497  uspgrex  49521  gzmulclALT  49742  bru3sqbru  49757  bru3sqez  49758  lmod1zrnlvec  49937  zlmodzxzldeplem1  49943  zlmodzxzldeplem3  49945  zlmodzxzldeplem4  49946  zlmodzxzldep  49947  ldepsnlinclem1  49948  ldepsnlinclem2  49949  blennn0elnn  50020  nn0sumshdiglemA  50062  nn0sumshdiglemB  50063  itcovalpclem2  50114  itcovalt2lem2  50119  ackval42  50139  rrx2line  50183  spheres  50189  2sphere  50192  2sphere0  50193  resipos  50420  functhinclem1  50910  prsthinc  50930  setc1oterm  50957  funcsetc1ocl  50962  funcsetc1o  50963  isinito2lem  50964  isinito3  50966  functermc2  50975  incat  51070  setc1onsubc  51071  parcatid2  51094  parcatid  51095  parmapfunc2  51105  par2diag  51111  fuconuniqlem  51112  fuconuniqvalslem  51114  tanh0  51251