Theorem eqeltri 2859

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

Syntax hints:   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  eqeltrri  2860  3eltr4i  2876  intab  4943  axrep6g  5251  unisn2  5275  inex2  5287  vpwex  5348  ord3ex  5358  zfpair  5392  vsnex  5406  snex  5410  opex  5445  opexOLD  5446  otex  5447  uniopel  5499  elvvuni  5738  isarep2  6625  fvex  6894  fvexi  6895  riotaex  7371  ovexi  7444  tpex  7743  oprabex  7969  oprabrexex2  7971  mpoexw  8071  mptmpoopabbrd  8074  tfrlem16  8376  1oex  8459  2oex  8461  1on  8462  2on  8463  3on  8466  4on  8467  oesuclem  8506  oecl  8518  o2p2e4  8522  nnecl  8595  1onnALT  8623  2onnALT  8625  3onn  8626  4onn  8627  mapsnf1o2  8888  sbthlem10  9080  cnvfi  9156  fnfi  9158  nnunifi  9247  pwfi  9274  prfiALT  9280  tpfi  9281  fczfsuppd  9342  cantnfvalf  9630  oemapwe  9659  cantnffval2  9660  cnfcom3clem  9670  ssttrcl  9680  r1fin  9741  scottex2  9867  hta  9879  infxpenlem  9993  alephon  10049  alephfplem1  10084  dfac5lem4  10106  dfac5lem5  10107  kmlem10  10139  fin1a2lem10  10388  fin1a2lem12  10390  hsmexlem9  10404  axcc2lem  10415  domtriomlem  10421  axdc2lem  10427  axcclem  10436  brdom7disj  10510  brdom6disj  10511  iundom2g  10519  konigthlem  10548  canthwelem  10630  wunex2  10718  wunex3  10721  1nq  10908  1pr  10995  nrex1  11044  axcnex  11127  ax1cn  11129  pnfex  11257  mnfxr  11261  cju  12209  nnexALT  12230  2nn  12309  2re  12310  2cn  12311  3nn  12315  3re  12316  3cn  12317  4nn  12319  4re  12320  4cn  12321  5nn  12322  5re  12323  5cn  12324  6nn  12325  6re  12326  6cn  12327  7nn  12328  7re  12329  7cn  12330  8nn  12331  8re  12332  8cn  12333  9nn  12334  9re  12335  9cn  12336  nn0ex  12505  zexALT  12606  nneo  12675  zeo  12677  deccl  12721  10re  12729  decnncl  12730  numnncl2  12734  decnncl2  12735  numsucc  12751  numma2c  12757  numadd  12758  numaddc  12759  nummul1c  12760  nummul2c  12761  decmul1  12775  qexALT  12983  xrex  13006  xnegex  13229  xnegcl  13234  ixxssxr  13379  fz0to4untppr  13654  fz0to5un2tp  13655  om2uzuzi  13981  ltweuz  13993  axdc4uzlem  14015  seqex  14035  seqexw  14049  m1expcl2  14117  faccl  14315  facwordi  14321  faclbnd2  14323  bccl  14354  hashen1  14402  hashrabrsn  14404  hashunlei  14458  hashpw  14469  tpf1o  14534  s1cli  14639  ccat2s1p1  14663  cats1un  14754  revs1  14798  cshwsexa  14857  cats1cli  14890  cats1fvn  14891  crre  15161  remim  15164  climmpt  15618  sumex  15735  supcvg  15906  geo2lim  15925  prodex  15955  bpoly4  16108  ere  16138  eftlub  16160  efsep  16161  tan0  16202  ef01bndlem  16235  nn0o  16436  divalglem5  16450  divalglem9  16454  sadcf  16506  smupf  16531  crth  16832  phimullem  16833  pczpre  16902  pockthi  16962  prmreclem2  16972  igz  16989  0ramcl  17078  1259lem1  17186  1259lem2  17187  1259lem3  17188  1259lem4  17189  1259lem5  17190  1259prm  17191  2503lem1  17192  2503lem2  17193  2503lem3  17194  2503prm  17195  4001lem1  17196  4001lem2  17197  4001lem3  17198  4001lem4  17199  4001prm  17200  strle1  17213  ndxarg  17251  basendxnn  17274  plusgndxnn  17333  tsetndxnn  17402  plendxnn  17416  dsndxnn  17435  unifndxnn  17445  prdsbasex  17498  prdsds  17512  yonedalem3  18331  isposix  18375  chnub  18673  plusffval  18699  issubmgm2  18756  efmnd1hash  18946  efmnd2hash  18948  smndex1bas  18963  smndex1sgrp  18965  smndex1mnd  18967  smndex1id  18968  smndex2dbas  18971  smndex2hbas  18973  grpsubfval  19045  mulgfval  19130  symg1hash  19455  symg2hash  19457  symgvalstruct  19462  symgfisg  19533  psgnsn  19585  psgnprfval1  19587  odfval  19597  sylow2alem2  19683  efgsval2  19798  efgsp1  19802  pgpfaclem1  20148  dvdsrval  20439  isirred  20497  scaffval  21001  prmidl0  21478  cnfldex  21525  xrsex  21539  pzriprnglem4  21634  pzriprnglem5  21635  pzriprnglem6  21636  pzriprng1ALT  21646  znle  21686  znidomb  21711  cnmsgnsubg  21727  refld  21769  ipffval  21798  psrbag0  22213  psrbagsn  22214  psr1baslem  22345  mat1dimbas  22629  mat1dimscm  22632  mat1f1o  22635  mat1rhmelval  22637  m2detleib  22788  pmatcoe1fsupp  22858  indistopon  23158  iccordt  23371  conncompid  23588  ptbasfi  23738  ptcmpfi  23970  ustfn  24359  ust0  24377  ustn0  24378  tmslem  24639  nmfval  24745  cnbl0  24930  cnopn  24943  remet  24947  re2ndc  24958  zcld  24971  icccmp  24983  xrge0gsumle  24991  xrge0tsms  24992  xmetdcn  24996  divcn  25027  expcn  25031  iiconn  25046  idcncf  25077  cnmpopc  25087  cnrehmeo  25112  cnheiborlem  25113  rellycmp  25116  bndth  25117  evth2  25119  cnrlmod  25302  cnrlvec  25303  cncmet  25481  ishl2  25529  ehleudis  25577  ehleudisval  25578  finiunmbl  25703  ioombl1lem4  25720  vitalilem4  25770  vitalilem5  25771  ismbf2d  25799  mbfimaopnlem  25814  mbfi1fseqlem6  25879  itgex  25929  bddmulibl  25998  ditgex  26011  recnperf  26064  dvcnvrelem2  26177  ftc1  26201  mdegcl  26226  plyeq0lem  26367  aaliou3lem4  26509  dvradcnv  26584  sincn  26607  coscn  26608  tanabsge  26671  circsubm  26718  reloggim  26764  logcn  26812  dvloglem  26813  logdmopn  26814  dvlog2  26818  2irrexpq  26896  cxpcn  26910  cxpcn3  26913  resqrtcn  26914  2logb9irrALT  26963  2irrexpqALT  26965  atanrecl  27076  atan1  27093  atansopn  27097  birthdaylem1  27116  birthday  27119  emcllem4  27163  emcllem6  27165  lgamgulmlem6  27198  basellem6  27250  ppiublem1  27366  bposlem6  27453  bposlem8  27455  lgslem4  27464  lgsdir2lem2  27490  selberglem1  27709  selberglem3  27711  selberg  27712  selbergs  27738  qdrng  27784  0no  28002  1no  28003  lrrecse  28135  precsexlem11  28410  seqsex  28478  nnsex  28511  n0bday  28545  n0subs  28556  n0p1nns  28564  dfnns2  28565  zsex  28573  bdayfinbndlem1  28660  z12sex  28667  z12shalf  28673  edgfndxnn  29342  structvtxvallem  29370  usgrexmpllem  29610  usgrexmpl  29613  uhgrspan1  29653  upgrres  29656  umgrres  29657  usgrres  29658  upgrres1  29663  umgrres1  29664  usgrres1  29665  fusgrfis  29680  cusgrres  29798  vtxdlfgrval  29835  vtxdusgr0edgnelALT  29846  umgr2v2e  29875  vtxdginducedm1lem1  29889  vtxdginducedm1fi  29894  finsumvtxdg2ssteplem4  29898  pthdlem1  30115  crctcshlem3  30168  2wlkd  30285  2wlkond  30286  2trlond  30288  2pthd  30289  2pthond  30291  umgr2adedgwlkonALT  30296  0pth  30476  wlk2v2e  30508  3wlkd  30521  3trlond  30524  3pthd  30525  3pthond  30526  3spthond  30528  eupthvdres  30586  eulerpathpr  30591  konigsbergumgr  30602  konigsberglem5  30607  konigsberg  30608  ex-lcm  30809  isvciOLD  30932  isnvi  30965  blocni  31157  hmoval  31162  cncph  31171  ipasslem7  31188  siilem2  31204  normlem2  31463  normlem3  31464  normlem6  31467  h0elch  31607  hhssabloilem  31613  hhsssh  31621  spansnji  31998  nonbooli  32003  3oalem5  32018  3oalem6  32019  3oai  32020  mayetes3i  32081  nmcexi  32378  nmbdfnlb  32402  rnelshi  32411  cnlnadjlem5  32423  pjbdlni  32501  golem2  32624  goeqi  32625  dp2clq  33200  rpdp2cl  33201  rpdp2cl2  33202  dpmul100  33216  rpdpcl  33222  xrge0tsmsd  33393  pmtrto1cl  33419  psgnfzto1stlem  33420  fzto1st  33423  psgnfzto1st  33425  nn0omnd  33664  xrge0slmod  33668  qusima  33717  fply1  33848  extvfvcl  33926  ply1degltdimlem  34012  ccfldextdgrr  34062  algextdeglem8  34114  constrfin  34136  2sqr3minply  34170  2sqr3nconstr  34171  cos9thpiminplylem4  34175  cos9thpiminplylem5  34176  cos9thpinconstrlem2  34180  circtopn  34227  circcn  34228  zarcmplem  34271  tpr2tp  34294  tpr2rico  34302  ordtprsval  34308  ordtprsuni  34309  ordtrestNEW  34311  ordtrest2NEWlem  34312  ordtrest2NEW  34313  ordtconnlem1  34314  mndpluscn  34316  xrge0pluscn  34330  xrge0mulc1cn  34331  xrge0haus  34334  lmlimxrge0  34338  lmxrge0  34342  qqhcn  34381  qqhucn  34382  esumex  34419  esumcst  34453  hasheuni  34475  esumcvg  34476  prsiga  34521  brsiga  34573  mbfmcnt  34658  sxbrsigalem3  34662  dya2iocuni  34673  dya2iocucvr  34674  sxbrsigalem1  34675  sxbrsiga  34680  eulerpartlemt  34761  fibp1  34791  coinflipprob  34870  coinfliprv  34873  ccatmulgnn0dir  34932  signswplusg  34942  hgt750lem2  35039  hgt750leme  35045  bnj105  35113  bnj918  35155  bnj95  35252  bnj852  35309  bnj865  35311  fineqvnttrclse  35537  subfacp1lem1  35671  subfacp1lem3  35674  subfacp1lem5  35676  subfacp1lem6  35677  kur14lem7  35704  iisconn  35744  iillysconn  35745  cvmliftlem5  35781  cvmliftlem8  35784  cvmliftlem10  35786  cvmlift2lem9  35803  satfv0  35850  goalrlem  35888  goalr  35889  satffunlem2lem2  35898  circum  36166  iexpire  36227  altopex  36452  colinearex  36552  ssoninhaus  36959  cnndvlem2  37127  bj-prex  37676  bj-prfromadj  37681  bj-pinftyccb  37865  taupi  37967  isbasisrelowl  38004  relowlpssretop  38010  poimirlem29  38300  poimirlem30  38301  poimirlem31  38302  dvasin  38355  dvacos  38356  areacirc  38364  upixp  38380  fdc  38396  lmclim2  38409  cncfres  38416  heibor1lem  38460  rrnval  38478  rrnmet  38480  reheibor  38490  isdrngo2  38609  isrngohom  38616  idlval  38664  isidl  38665  igenval  38712  scottexf  38817  cnvepresex  38985  preex  39141  renegclALT  39737  ldualfvadd  39902  cmtfvalN  39984  cvrfval  40042  cdleme31fv  41164  cdlemk40  41691  cdlemk56  41745  dibopelvalN  41917  dibopelval2  41919  dibelval3  41921  diblsmopel  41945  cdlemn11a  41981  dihopelvalcpre  42022  dihpN  42110  hlhilsca  42709  hlhilip  42722  3factsumint1  42788  lcmineqlem23  42818  aks4d1p1p6  42840  aks4d1p1p5  42842  aks6d1c6isolem2  42942  25or6to4  42973  itrere  43079  acos1half  43119  redvmptabs  43121  readvrec2  43122  sn-0tie0  43225  sn-itrere  43262  sn-retire  43263  prjspval  43335  flt4lem5e  43388  sn-isghm  43405  mapfzcons2  43450  jm2.23  43723  jm2.27dlem2  43737  jm2.27dlem4  43739  rmydioph  43741  rmxdioph  43743  expdiophlem2  43749  expdioph  43750  aomclem6  43786  pwslnmlem0  43818  frlmpwfi  43825  mncn0  43866  aaitgo  43889  arearect  43942  areaquad  43943  omcl3g  44061  comptiunov2i  44432  frege110  44699  frege133  44722  radcnvrat  45024  uzmptshftfval  45056  dvradcnv2  45057  binomcxplemdvbinom  45063  binomcxplemcvg  45064  binomcxplemnotnn0  45066  permaxinf2lem  45721  rfcnpre1  45739  fcnre  45745  refsumcn  45750  refsum2cnlem1  45757  unirnmapsn  45930  infxrpnf  46160  iocopn  46236  icoopn  46241  mccl  46314  clim1fr1  46317  islptre  46335  sumnnodd  46346  lptre2pt  46354  limclner  46365  limclr  46369  expfac  46371  0cnf  46591  icccncfext  46601  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  itgsin0pilem1  46664  iblempty  46679  itgvol0  46682  stoweidlem47  46761  stoweidlem53  46767  stoweidlem57  46771  stoweidlem59  46773  wallispilem3  46781  wallispilem4  46782  wallispilem5  46783  wallispi  46784  stirlinglem1  46788  stirlinglem8  46795  stirlinglem12  46799  stirlinglem13  46800  stirlinglem14  46801  stirlinglem15  46802  dirkerper  46810  dirkercncflem2  46818  fourierdlem16  46837  fourierdlem21  46842  fourierdlem22  46843  fourierdlem36  46857  fourierdlem42  46863  fourierdlem71  46891  fourierdlem83  46903  fourierdlem102  46922  fourierdlem103  46923  fourierdlem104  46924  fourierdlem111  46931  fourierdlem112  46932  fourierdlem114  46934  sqwvfoura  46942  sqwvfourb  46943  fourierswlem  46944  fouriersw  46945  etransclem48  46996  salexct3  47056  salgencntex  47057  salgensscntex  47058  iooborel  47065  bor1sal  47069  gsumge0cl  47085  sge0tsms  47094  sge0isum  47141  nnfoctbdjlem  47169  isomenndlem  47244  mbfresmf  47453  incsmflem  47455  incsmf  47456  smfmbfcex  47474  decsmflem  47480  decsmf  47481  smflimlem1  47485  smfpimbor1lem2  47513  smf2id  47515  smfco  47516  smfpimcclem  47521  goldrarr  47618  lambert0  47624  sprsymrelfolem1  48241  sprbisymrel  48248  fmtno0prm  48310  fmtno1prm  48311  fmtno2prm  48312  fmtno3prm  48314  fmtno4prm  48327  m2prm  48343  m3prm  48344  m5prm  48350  m7prm  48352  lighneallem4a  48360  nprmdvdsfacm1lem4  48375  0evenALTV  48453  1oddALTV  48455  2evenALTV  48457  6even  48476  7odd  48477  8even  48478  9gbo  48539  opstrgric  48691  ushggricedg  48692  grtri  48705  usgrexmpl1  48787  usgrexmpl1vtx  48788  usgrexmpl1edg  48789  usgrexmpl2  48792  usgrexmpl2vtx  48793  usgrexmpl2edg  48794  gpgprismgr4cycllem5  48864  pgnbgreunbgr  48890  pgn4cyclex  48891  uspgrex  48915  lmod1zrnlvec  49274  zlmodzxzldeplem1  49280  zlmodzxzldeplem3  49282  zlmodzxzldeplem4  49283  zlmodzxzldep  49284  ldepsnlinclem1  49285  ldepsnlinclem2  49286  blennn0elnn  49357  nn0sumshdiglemA  49399  nn0sumshdiglemB  49400  itcovalpclem2  49451  itcovalt2lem2  49456  ackval42  49476  rrx2line  49520  rrx2linesl  49523  spheres  49526  2sphere  49529  2sphere0  49530  line2x  49534  line2y  49535  resipos  49753  functhinclem1  50222  prsthinc  50242  setc1oterm  50269  funcsetc1ocl  50274  funcsetc1o  50275  isinito2lem  50276  isinito3  50278  functermc2  50287  incat  50379  setc1onsubc  50380