Theorem eqeltri 2861

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

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

This theorem is used by:  eqeltrri  2862  3eltr4i  2878  intab  4945  axrep6g  5253  unisn2  5277  inex2  5289  vpwex  5350  ord3ex  5360  zfpair  5394  vsnex  5408  snex  5412  opex  5447  opexOLD  5448  otex  5449  uniopel  5501  elvvuni  5740  isarep2  6629  fvex  6898  fvexi  6899  riotaex  7380  ovexi  7453  tpex  7753  oprabex  7979  oprabrexex2  7981  mpoexw  8081  mptmpoopabbrd  8084  tfrlem16  8386  1oex  8469  2oex  8471  1on  8472  2on  8473  3on  8476  4on  8477  oesuclem  8516  oecl  8528  o2p2e4  8532  nnecl  8605  1onnALT  8633  2onnALT  8635  3onn  8636  4onn  8637  mapsnf1o2  8898  sbthlem10  9091  cnvfi  9167  fnfi  9169  nnunifi  9258  pwfi  9285  prfiALT  9291  tpfi  9292  fczfsuppd  9353  cantnfvalf  9641  oemapwe  9670  cantnffval2  9671  cnfcom3clem  9681  ssttrcl  9691  r1fin  9752  scottex  9869  scottex2OLD  9882  hta  9898  htaOLD  9899  infxpenlem  10013  alephon  10069  alephfplem1  10104  dfac5lem4  10126  dfac5lem5  10127  kmlem10  10159  fin1a2lem10  10408  fin1a2lem12  10410  hsmexlem9  10424  axcc2lem  10435  domtriomlem  10441  axdc2lem  10447  axcclem  10456  brdom7disj  10530  brdom6disj  10531  iundom2g  10539  konigthlem  10568  canthwelem  10650  wunex2  10738  wunex3  10741  1nq  10928  1pr  11015  nrex1  11064  axcnex  11147  ax1cn  11149  pnfex  11277  mnfxr  11281  cju  12229  nnexALT  12250  2nn  12329  2re  12330  2cn  12331  3nn  12335  3re  12336  3cn  12337  4nn  12339  4re  12340  4cn  12341  5nn  12342  5re  12343  5cn  12344  6nn  12345  6re  12346  6cn  12347  7nn  12348  7re  12349  7cn  12350  8nn  12351  8re  12352  8cn  12353  9nn  12354  9re  12355  9cn  12356  nn0ex  12525  zexALT  12626  nneo  12696  zeo  12698  deccl  12742  10re  12750  decnncl  12751  numnncl2  12755  decnncl2  12756  numsucc  12772  numma2c  12778  numadd  12779  numaddc  12780  nummul1c  12781  nummul2c  12782  decmul1  12796  qexALT  13004  xrex  13027  xnegex  13250  xnegcl  13255  ixxssxr  13400  fz0to4untppr  13675  fz0to5un2tp  13676  om2uzuzi  14003  ltweuz  14015  axdc4uzlem  14037  seqex  14057  seqexw  14071  m1expcl2  14139  faccl  14337  facwordi  14343  faclbnd2  14345  bccl  14376  hashen1  14424  hashrabrsn  14426  hashunlei  14480  hashpw  14491  tpf1o  14556  s1cli  14662  ccat2s1p1  14687  cats1un  14780  revs1  14824  cshwsexa  14885  cats1cli  14918  cats1fvn  14919  crre  15189  remim  15192  climmpt  15646  sumex  15763  supcvg  15933  geo2lim  15952  prodex  15982  bpoly4  16135  ere  16165  eftlub  16187  efsep  16188  tan0  16229  ef01bndlem  16262  nn0o  16463  divalglem5  16477  divalglem9  16481  sadcf  16533  smupf  16558  crth  16859  phimullem  16860  pczpre  16929  pockthi  16989  prmreclem2  16999  igz  17016  0ramcl  17105  1259lem1  17213  1259lem2  17214  1259lem3  17215  1259lem4  17216  1259lem5  17217  1259prm  17218  2503lem1  17219  2503lem2  17220  2503lem3  17221  2503prm  17222  4001lem1  17223  4001lem2  17224  4001lem3  17225  4001lem4  17226  4001prm  17227  strle1  17240  ndxarg  17278  basendxnn  17301  plusgndxnn  17360  tsetndxnn  17429  plendxnn  17443  dsndxnn  17462  unifndxnn  17472  prdsbasex  17525  prdsds  17539  yonedalem3  18358  isposix  18402  chnub  18700  plusffval  18726  issubmgm2  18793  efmnd1hash  18988  efmnd2hash  18990  smndex1bas  19005  smndex1sgrp  19007  smndex1mnd  19009  smndex1id  19010  smndex2dbas  19013  smndex2hbas  19015  grpsubfval  19094  mulgfval  19179  symg1hash  19504  symg2hash  19506  symgvalstruct  19511  symgfisg  19582  psgnsn  19634  psgnprfval1  19636  odfval  19646  sylow2alem2  19732  efgsval2  19847  efgsp1  19851  pgpfaclem1  20197  dvdsrval  20489  isirred  20547  scaffval  21051  prmidl0  21528  cnfldex  21575  xrsex  21589  pzriprnglem4  21684  pzriprnglem5  21685  pzriprnglem6  21686  pzriprng1ALT  21696  znle  21736  znidomb  21761  cnmsgnsubg  21777  refld  21819  ipffval  21848  psrbag0  22263  psrbagsn  22264  psr1baslem  22395  mat1dimbas  22679  mat1dimscm  22682  mat1f1o  22685  mat1rhmelval  22687  m2detleib  22838  pmatcoe1fsupp  22908  indistopon  23208  iccordt  23421  conncompid  23638  ptbasfi  23789  ptcmpfi  24021  ustfn  24410  ust0  24428  ustn0  24429  tmslem  24690  nmfval  24796  cnbl0  24981  cnopn  24994  remet  24998  re2ndc  25009  zcld  25022  icccmp  25034  xrge0gsumle  25042  xrge0tsms  25043  xmetdcn  25047  divcn  25078  expcn  25082  iiconn  25097  idcncf  25128  cnmpopc  25138  cnrehmeo  25163  cnheiborlem  25164  rellycmp  25167  bndth  25168  evth2  25170  cnrlmod  25353  cnrlvec  25354  cncmet  25532  ishl2  25580  ehleudis  25628  ehleudisval  25629  finiunmbl  25754  ioombl1lem4  25771  vitalilem4  25821  vitalilem5  25822  ismbf2d  25850  mbfimaopnlem  25865  mbfi1fseqlem6  25930  itgex  25980  bddmulibl  26049  ditgex  26062  recnperf  26115  dvcnvrelem2  26228  ftc1  26252  mdegcl  26277  plyeq0lem  26418  aaliou3lem4  26560  dvradcnv  26635  sincn  26658  coscn  26659  tanabsge  26722  circsubm  26769  reloggim  26815  logcn  26863  dvloglem  26864  logdmopn  26865  dvlog2  26869  2irrexpq  26947  cxpcn  26961  cxpcn3  26964  resqrtcn  26965  2logb9irrALT  27014  2irrexpqALT  27016  atanrecl  27127  atan1  27144  atansopn  27148  birthdaylem1  27167  birthday  27170  emcllem4  27214  emcllem6  27216  lgamgulmlem6  27249  basellem6  27301  ppiublem1  27417  bposlem6  27504  bposlem8  27506  lgslem4  27515  lgsdir2lem2  27541  selberglem1  27760  selberglem3  27762  selberg  27763  selbergs  27789  qdrng  27835  0no  28053  1no  28054  lrrecse  28186  precsexlem11  28461  seqsex  28529  nnsex  28562  n0bday  28596  n0subs  28607  n0p1nns  28615  dfnns2  28616  zsex  28624  bdayfinbndlem1  28711  z12sex  28718  z12shalf  28724  edgfndxnn  29397  structvtxvallem  29425  usgrexmpllem  29668  usgrexmpl  29671  uhgrspan1  29711  upgrres  29714  umgrres  29715  usgrres  29716  upgrres1  29721  umgrres1  29722  usgrres1  29723  fusgrfis  29738  cusgrres  29856  vtxdlfgrval  29893  vtxdusgr0edgnelALT  29904  umgr2v2e  29933  vtxdginducedm1lem1  29947  vtxdginducedm1fi  29952  finsumvtxdg2ssteplem4  29956  pthdlem1  30179  crctcshlem3  30235  2wlkd  30352  2wlkond  30353  2trlond  30355  2pthd  30356  2pthond  30358  umgr2adedgwlkonALT  30363  0pth  30543  wlk2v2e  30579  3wlkd  30592  3trlond  30595  3pthd  30596  3pthond  30597  3spthond  30599  eupthvdres  30657  eulerpathpr  30662  konigsbergumgr  30673  konigsberglem5  30678  konigsberg  30679  ex-lcm  30880  isvciOLD  31003  isnvi  31036  blocni  31228  hmoval  31233  cncph  31242  ipasslem7  31259  siilem2  31275  normlem2  31534  normlem3  31535  normlem6  31538  h0elch  31678  hhssabloilem  31684  hhsssh  31692  spansnji  32069  nonbooli  32074  3oalem5  32089  3oalem6  32090  3oai  32091  mayetes3i  32152  nmcexi  32449  nmbdfnlb  32473  rnelshi  32482  cnlnadjlem5  32494  pjbdlni  32572  golem2  32695  goeqi  32696  dp2clq  33270  rpdp2cl  33271  rpdp2cl2  33272  dpmul100  33286  rpdpcl  33292  xrge0tsmsd  33457  pmtrto1cl  33483  psgnfzto1stlem  33484  fzto1st  33487  psgnfzto1st  33489  nn0omnd  33728  xrge0slmod  33732  qusima  33781  fply1  33912  extvfvcl  33990  ply1degltdimlem  34076  ccfldextdgrr  34126  algextdeglem8  34178  constrfin  34200  2sqr3minply  34234  2sqr3nconstr  34235  cos9thpiminplylem4  34239  cos9thpiminplylem5  34240  cos9thpinconstrlem2  34244  circtopn  34291  circcn  34292  zarcmplem  34335  tpr2tp  34358  tpr2rico  34366  ordtprsval  34372  ordtprsuni  34373  ordtrestNEW  34375  ordtrest2NEWlem  34376  ordtrest2NEW  34377  ordtconnlem1  34378  mndpluscn  34380  xrge0pluscn  34394  xrge0mulc1cn  34395  xrge0haus  34398  lmlimxrge0  34402  lmxrge0  34406  qqhcn  34445  qqhucn  34446  esumex  34483  esumcst  34517  hasheuni  34539  esumcvg  34540  prsiga  34585  brsiga  34638  mbfmcnt  34723  sxbrsigalem3  34727  dya2iocuni  34738  dya2iocucvr  34739  sxbrsigalem1  34740  sxbrsiga  34745  eulerpartlemt  34826  fibp1  34856  coinflipprob  34935  coinfliprv  34938  ccatmulgnn0dir  34997  signswplusg  35007  hgt750lem2  35104  hgt750leme  35110  bnj105  35178  bnj918  35220  bnj95  35317  bnj852  35374  bnj865  35376  fineqvnttrclse  35594  subfacp1lem1  35708  subfacp1lem3  35711  subfacp1lem5  35713  subfacp1lem6  35714  kur14lem7  35741  iisconn  35781  iillysconn  35782  cvmliftlem5  35818  cvmliftlem8  35821  cvmliftlem10  35823  cvmlift2lem9  35840  satfv0  35887  goalrlem  35925  goalr  35926  satffunlem2lem2  35935  circum  36203  iexpire  36264  altopex  36489  colinearex  36589  ssoninhaus  37016  cnndvlem2  37184  bj-prex  37733  bj-prfromadj  37738  bj-pinftyccb  37922  taupi  38024  isbasisrelowl  38061  relowlpssretop  38067  poimirlem29  38357  poimirlem30  38358  poimirlem31  38359  dvasin  38412  dvacos  38413  areacirc  38421  upixp  38438  fdc  38454  lmclim2  38467  cncfres  38474  heibor1lem  38518  rrnval  38536  rrnmet  38538  reheibor  38548  isdrngo2  38667  isrngohom  38674  idlval  38722  isidl  38723  igenval  38770  scottexf  38875  cnvepresex  39043  preex  39199  renegclALT  39795  ldualfvadd  39960  cmtfvalN  40042  cvrfval  40100  cdleme31fv  41222  cdlemk40  41749  cdlemk56  41803  dibopelvalN  41975  dibopelval2  41977  dibelval3  41979  diblsmopel  42003  cdlemn11a  42039  dihopelvalcpre  42080  dihpN  42168  hlhilsca  42767  hlhilip  42780  3factsumint1  42846  lcmineqlem23  42876  aks4d1p1p6  42898  aks4d1p1p5  42900  aks6d1c6isolem2  43000  25or6to4  43031  itrere  43137  acos1half  43177  redvmptabs  43179  readvrec2  43180  sn-0tie0  43283  sn-itrere  43320  sn-retire  43321  prjspval  43393  flt4lem5e  43446  sn-isghm  43463  mapfzcons2  43508  jm2.23  43781  jm2.27dlem2  43795  jm2.27dlem4  43797  rmydioph  43799  rmxdioph  43801  expdiophlem2  43807  expdioph  43808  aomclem6  43844  pwslnmlem0  43876  frlmpwfi  43883  mncn0  43924  aaitgo  43947  arearect  44000  areaquad  44001  omcl3g  44119  comptiunov2i  44490  frege110  44757  frege133  44780  radcnvrat  45082  uzmptshftfval  45114  dvradcnv2  45115  binomcxplemdvbinom  45121  binomcxplemcvg  45122  binomcxplemnotnn0  45124  permaxinf2lem  45779  rfcnpre1  45797  fcnre  45803  refsumcn  45808  refsum2cnlem1  45815  unirnmapsn  45988  infxrpnf  46218  iocopn  46294  icoopn  46299  mccl  46372  clim1fr1  46375  islptre  46393  sumnnodd  46404  lptre2pt  46412  limclner  46423  limclr  46427  expfac  46429  0cnf  46649  icccncfext  46659  ioodvbdlimc1lem2  46704  ioodvbdlimc2lem  46706  itgsin0pilem1  46722  iblempty  46737  itgvol0  46740  stoweidlem47  46819  stoweidlem53  46825  stoweidlem57  46829  stoweidlem59  46831  wallispilem3  46839  wallispilem4  46840  wallispilem5  46841  wallispi  46842  stirlinglem1  46846  stirlinglem8  46853  stirlinglem12  46857  stirlinglem13  46858  stirlinglem14  46859  stirlinglem15  46860  dirkerper  46868  dirkercncflem2  46876  fourierdlem16  46895  fourierdlem21  46900  fourierdlem22  46901  fourierdlem36  46915  fourierdlem42  46921  fourierdlem71  46949  fourierdlem83  46961  fourierdlem102  46980  fourierdlem103  46981  fourierdlem104  46982  fourierdlem111  46989  fourierdlem112  46990  fourierdlem114  46992  sqwvfoura  47000  sqwvfourb  47001  fourierswlem  47002  fouriersw  47003  etransclem48  47054  salexct3  47114  salgencntex  47115  salgensscntex  47116  iooborel  47123  bor1sal  47127  gsumge0cl  47143  sge0tsms  47152  sge0isum  47199  nnfoctbdjlem  47227  isomenndlem  47302  mbfresmf  47511  incsmflem  47513  incsmf  47514  smfmbfcex  47532  decsmflem  47538  decsmf  47539  smflimlem1  47543  smfpimbor1lem2  47571  smf2id  47573  smfco  47574  smfpimcclem  47579  goldrarr  47676  lambert0  47682  sprsymrelfolem1  48299  sprbisymrel  48306  fmtno0prm  48368  fmtno1prm  48369  fmtno2prm  48370  fmtno3prm  48372  fmtno4prm  48385  m2prm  48401  m3prm  48402  m5prm  48408  m7prm  48410  lighneallem4a  48418  nprmdvdsfacm1lem4  48433  0evenALTV  48511  1oddALTV  48513  2evenALTV  48515  6even  48534  7odd  48535  8even  48536  9gbo  48597  opstrgric  48749  ushggricedg  48750  grtri  48763  usgrexmpl1  48845  usgrexmpl1vtx  48846  usgrexmpl1edg  48847  usgrexmpl2  48850  usgrexmpl2vtx  48851  usgrexmpl2edg  48852  gpgprismgr4cycllem5  48922  pgnbgreunbgr  48948  pgn4cyclex  48949  uspgrex  48973  lmod1zrnlvec  49331  zlmodzxzldeplem1  49337  zlmodzxzldeplem3  49339  zlmodzxzldeplem4  49340  zlmodzxzldep  49341  ldepsnlinclem1  49342  ldepsnlinclem2  49343  blennn0elnn  49414  nn0sumshdiglemA  49456  nn0sumshdiglemB  49457  itcovalpclem2  49508  itcovalt2lem2  49513  ackval42  49533  rrx2line  49577  rrx2linesl  49580  spheres  49583  2sphere  49586  2sphere0  49587  line2x  49591  line2y  49592  resipos  49810  functhinclem1  50279  prsthinc  50299  setc1oterm  50326  funcsetc1ocl  50331  funcsetc1o  50332  isinito2lem  50333  isinito3  50335  functermc2  50344  incat  50436  setc1onsubc  50437