Theorem eqeltri 2824

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

Syntax hints:   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  eqeltrri  2825  3eltr4i  2841  intab  4928  axrep6g  5229  unisn2  5251  inex2  5257  vpwex  5316  ord3ex  5326  zfpair  5360  vsnex  5373  opex  5407  otex  5408  uniopel  5459  elvvuni  5696  isarep2  6572  fvex  6835  fvexi  6836  riotaex  7310  ovexi  7383  tpex  7682  oprabex  7911  oprabrexex2  7913  mpoexw  8013  mptmpoopabbrd  8015  mptmpoopabbrdOLD  8016  tfrlem16  8315  1oex  8398  2oex  8399  1on  8400  2on  8401  3on  8404  4on  8405  oesuclem  8443  oecl  8455  o2p2e4  8459  nnecl  8531  1onnALT  8559  2onnALT  8561  3onn  8562  4onn  8563  mapsnf1o2  8821  sbthlem10  9013  cnvfi  9090  fnfi  9092  nnunifi  9180  imafiOLD  9205  pwfi  9208  prfiALT  9214  tpfi  9215  fczfsuppd  9276  cantnfvalf  9561  oemapwe  9590  cantnffval2  9591  cnfcom3clem  9601  ssttrcl  9611  r1fin  9669  hta  9793  infxpenlem  9907  alephon  9963  alephfplem1  9998  dfac5lem4  10020  dfac5lem5  10021  dfac5lem4OLD  10022  kmlem10  10054  fin1a2lem10  10303  fin1a2lem12  10305  hsmexlem9  10319  axcc2lem  10330  domtriomlem  10336  axdc2lem  10342  axcclem  10351  brdom7disj  10425  brdom6disj  10426  iundom2g  10434  konigthlem  10462  canthwelem  10544  wunex2  10632  wunex3  10635  1nq  10822  1pr  10909  nrex1  10958  axcnex  11041  ax1cn  11043  pnfex  11168  mnfxr  11172  cju  12124  nnexALT  12130  2nn  12201  2re  12202  2cn  12203  3nn  12207  3re  12208  3cn  12209  4nn  12211  4re  12212  4cn  12213  5nn  12214  5re  12215  5cn  12216  6nn  12217  6re  12218  6cn  12219  7nn  12220  7re  12221  7cn  12222  8nn  12223  8re  12224  8cn  12225  9nn  12226  9re  12227  9cn  12228  nn0ex  12390  zexALT  12491  nneo  12560  zeo  12562  deccl  12606  10re  12610  decnncl  12611  numnncl2  12614  decnncl2  12615  numsucc  12631  numma2c  12637  numadd  12638  numaddc  12639  nummul1c  12640  nummul2c  12641  decmul1  12655  qexALT  12865  xrex  12888  xnegex  13110  xnegcl  13115  ixxssxr  13260  fz0to4untppr  13533  fz0to5un2tp  13534  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  14512  ccat2s1p1  14536  cats1un  14627  revs1  14671  cshwsexa  14730  cshwsexaOLD  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  plusffval  18520  issubmgm2  18577  efmnd1hash  18766  efmnd2hash  18768  smndex1bas  18780  smndex1sgrp  18782  smndex1mnd  18784  smndex1id  18785  smndex2dbas  18788  smndex2hbas  18790  grpsubfval  18862  mulgfval  18948  symg1hash  19269  symg2hash  19271  symgvalstruct  19276  symgfisg  19347  psgnsn  19399  psgnprfval1  19401  odfval  19411  sylow2alem2  19497  efgsval2  19612  efgsp1  19616  pgpfaclem1  19962  dvdsrval  20246  isirred  20304  scaffval  20783  cnfldex  21264  xrsex  21291  pzriprnglem4  21391  pzriprnglem5  21392  pzriprnglem6  21393  pzriprng1ALT  21403  znle  21443  znidomb  21468  cnmsgnsubg  21484  refld  21526  ipffval  21555  psrbag0  21967  psrbagsn  21968  psr1baslem  22067  mat1dimbas  22357  mat1dimscm  22360  mat1f1o  22363  mat1rhmelval  22365  m2detleib  22516  pmatcoe1fsupp  22586  indistopon  22886  iccordt  23099  conncompid  23316  ptbasfi  23466  ptcmpfi  23698  ustfn  24087  ust0  24105  ustn0  24106  tmslem  24368  nmfval  24474  cnbl0  24659  cnopn  24672  remet  24676  re2ndc  24687  zcld  24700  icccmp  24712  xrge0gsumle  24720  xrge0tsms  24721  xmetdcn  24725  divcnOLD  24755  divcn  24757  expcn  24761  expcnOLD  24763  iiconn  24778  idcncf  24809  cnmpopc  24820  cnrehmeo  24849  cnrehmeoOLD  24850  cnheiborlem  24851  rellycmp  24854  bndth  24855  evth2  24857  cnrlmod  25041  cnrlvec  25042  cncmet  25220  ishl2  25268  ehleudis  25316  ehleudisval  25317  finiunmbl  25443  ioombl1lem4  25460  vitalilem4  25510  vitalilem5  25511  ismbf2d  25539  mbfimaopnlem  25554  mbfi1fseqlem6  25619  itgex  25669  bddmulibl  25738  ditgex  25751  recnperf  25804  dvcnvrelem2  25921  ftc1  25947  mdegcl  25972  plyeq0lem  26113  aaliou3lem4  26252  dvradcnv  26328  sincn  26352  coscn  26353  tanabsge  26413  circsubm  26460  reloggim  26506  logcn  26554  dvloglem  26555  logdmopn  26556  dvlog2  26560  2irrexpq  26638  cxpcn  26652  cxpcnOLD  26653  cxpcn3  26656  resqrtcn  26657  2logb9irrALT  26706  2irrexpqALT  26708  atanrecl  26819  atan1  26836  atansopn  26840  birthdaylem1  26859  birthday  26862  emcllem4  26907  emcllem6  26909  lgamgulmlem6  26942  basellem6  26994  ppiublem1  27111  bposlem6  27198  bposlem8  27200  lgslem4  27209  lgsdir2lem2  27235  selberglem1  27454  selberglem3  27456  selberg  27457  selbergs  27483  qdrng  27529  0sno  27740  1sno  27741  lrrecse  27854  precsexlem11  28124  seqsex  28184  nnsex  28216  n0sbday  28249  n0subs  28258  n0p1nns  28265  dfnns2  28266  zsex  28273  zs12ex  28351  zs12half  28357  edgfndxnn  28937  structvtxvallem  28965  usgrexmpllem  29205  usgrexmpl  29208  uhgrspan1  29248  upgrres  29251  umgrres  29252  usgrres  29253  upgrres1  29258  umgrres1  29259  usgrres1  29260  fusgrfis  29275  cusgrres  29394  vtxdlfgrval  29431  vtxdusgr0edgnelALT  29442  umgr2v2e  29471  vtxdginducedm1lem1  29485  vtxdginducedm1fi  29490  finsumvtxdg2ssteplem4  29494  pthdlem1  29711  crctcshlem3  29764  2wlkd  29881  2wlkond  29882  2trlond  29884  2pthd  29885  2pthond  29887  umgr2adedgwlkonALT  29892  0pth  30069  wlk2v2e  30101  3wlkd  30114  3trlond  30117  3pthd  30118  3pthond  30119  3spthond  30121  eupthvdres  30179  eulerpathpr  30184  konigsbergumgr  30195  konigsberglem5  30200  konigsberg  30201  ex-lcm  30402  isvciOLD  30524  isnvi  30557  blocni  30749  hmoval  30754  cncph  30763  ipasslem7  30780  siilem2  30796  normlem2  31055  normlem3  31056  normlem6  31059  h0elch  31199  hhssabloilem  31205  hhsssh  31213  spansnji  31590  nonbooli  31595  3oalem5  31610  3oalem6  31611  3oai  31612  mayetes3i  31673  nmcexi  31970  nmbdfnlb  31994  rnelshi  32003  cnlnadjlem5  32015  pjbdlni  32093  golem2  32216  goeqi  32217  dp2clq  32821  rpdp2cl  32822  rpdp2cl2  32823  dpmul100  32837  rpdpcl  32843  chnub  32954  xrge0tsmsd  33015  pmtrto1cl  33041  psgnfzto1stlem  33042  fzto1st  33045  psgnfzto1st  33047  nn0omnd  33282  xrge0slmod  33285  qusima  33345  prmidl0  33387  fply1  33493  ply1degltdimlem  33589  ccfldextdgrr  33639  algextdeglem8  33691  constrfin  33713  2sqr3minply  33747  2sqr3nconstr  33748  cos9thpiminplylem4  33752  cos9thpiminplylem5  33753  cos9thpinconstrlem2  33757  circtopn  33804  circcn  33805  zarcmplem  33848  tpr2tp  33871  tpr2rico  33879  ordtprsval  33885  ordtprsuni  33886  ordtrestNEW  33888  ordtrest2NEWlem  33889  ordtrest2NEW  33890  ordtconnlem1  33891  mndpluscn  33893  xrge0pluscn  33907  xrge0mulc1cn  33908  xrge0haus  33911  lmlimxrge0  33915  lmxrge0  33919  qqhcn  33958  qqhucn  33959  esumex  33996  esumcst  34030  hasheuni  34052  esumcvg  34053  prsiga  34098  brsiga  34150  mbfmcnt  34236  sxbrsigalem3  34240  dya2iocuni  34251  dya2iocucvr  34252  sxbrsigalem1  34253  sxbrsiga  34258  eulerpartlemt  34339  fibp1  34369  coinflipprob  34448  coinfliprv  34451  ccatmulgnn0dir  34510  signswplusg  34523  hgt750lem2  34620  hgt750leme  34626  bnj105  34691  bnj918  34733  bnj95  34831  bnj852  34888  bnj865  34890  subfacp1lem1  35152  subfacp1lem3  35155  subfacp1lem5  35157  subfacp1lem6  35158  kur14lem7  35185  iisconn  35225  iillysconn  35226  cvmliftlem5  35262  cvmliftlem8  35265  cvmliftlem10  35267  cvmlift2lem9  35284  satfv0  35331  goalrlem  35369  goalr  35370  satffunlem2lem2  35379  circum  35647  iexpire  35708  altopex  35934  colinearex  36034  ssoninhaus  36422  cnndvlem2  36512  bj-prex  37014  bj-prfromadj  37019  bj-pinftyccb  37195  taupi  37297  isbasisrelowl  37332  relowlpssretop  37338  poimirlem29  37629  poimirlem30  37630  poimirlem31  37631  dvasin  37684  dvacos  37685  areacirc  37693  upixp  37709  fdc  37725  lmclim2  37738  cncfres  37745  heibor1lem  37789  rrnval  37807  rrnmet  37809  reheibor  37819  isdrngo2  37938  isrngohom  37945  idlval  37993  isidl  37994  igenval  38041  scottexf  38148  cnvepresex  38304  renegclALT  38942  ldualfvadd  39107  cmtfvalN  39189  cvrfval  39247  cdleme31fv  40369  cdlemk40  40896  cdlemk56  40950  dibopelvalN  41122  dibopelval2  41124  dibelval3  41126  diblsmopel  41150  cdlemn11a  41186  dihopelvalcpre  41227  dihpN  41315  hlhilsca  41914  hlhilip  41927  3factsumint1  41994  lcmineqlem23  42024  aks4d1p1p6  42046  aks4d1p1p5  42048  aks6d1c6isolem2  42148  itrere  42291  acos1half  42331  redvmptabs  42333  readvrec2  42334  sn-0tie0  42424  sn-itrere  42461  sn-retire  42462  prjspval  42576  flt4lem5e  42629  sn-isghm  42646  mapfzcons2  42692  jm2.23  42969  jm2.27dlem2  42983  jm2.27dlem4  42985  rmydioph  42987  rmxdioph  42989  expdiophlem2  42995  expdioph  42996  aomclem6  43032  pwslnmlem0  43064  frlmpwfi  43071  mncn0  43112  aaitgo  43135  arearect  43188  areaquad  43189  omcl3g  43307  comptiunov2i  43679  frege110  43946  frege133  43969  scottex2  44218  radcnvrat  44287  uzmptshftfval  44319  dvradcnv2  44320  binomcxplemdvbinom  44326  binomcxplemcvg  44327  binomcxplemnotnn0  44329  permaxinf2lem  44986  rfcnpre1  44997  fcnre  45003  refsumcn  45008  refsum2cnlem1  45015  unirnmapsn  45192  infxrpnf  45425  iocopn  45501  icoopn  45506  mccl  45579  clim1fr1  45582  islptre  45600  sumnnodd  45611  lptre2pt  45621  limclner  45632  limclr  45636  expfac  45638  0cnf  45858  icccncfext  45868  ioodvbdlimc1lem2  45913  ioodvbdlimc2lem  45915  itgsin0pilem1  45931  iblempty  45946  itgvol0  45949  stoweidlem47  46028  stoweidlem53  46034  stoweidlem57  46038  stoweidlem59  46040  wallispilem3  46048  wallispilem4  46049  wallispilem5  46050  wallispi  46051  stirlinglem1  46055  stirlinglem8  46062  stirlinglem12  46066  stirlinglem13  46067  stirlinglem14  46068  stirlinglem15  46069  dirkerper  46077  dirkercncflem2  46085  fourierdlem16  46104  fourierdlem21  46109  fourierdlem22  46110  fourierdlem36  46124  fourierdlem42  46130  fourierdlem71  46158  fourierdlem83  46170  fourierdlem102  46189  fourierdlem103  46190  fourierdlem104  46191  fourierdlem111  46198  fourierdlem112  46199  fourierdlem114  46201  sqwvfoura  46209  sqwvfourb  46210  fourierswlem  46211  fouriersw  46212  etransclem48  46263  salexct3  46323  salgencntex  46324  salgensscntex  46325  iooborel  46332  bor1sal  46336  gsumge0cl  46352  sge0tsms  46361  sge0isum  46408  nnfoctbdjlem  46436  isomenndlem  46511  mbfresmf  46720  incsmflem  46722  incsmf  46723  smfmbfcex  46741  decsmflem  46747  decsmf  46748  smflimlem1  46752  smfpimbor1lem2  46780  smf2id  46782  smfco  46783  smfpimcclem  46788  tworepnotupword  46867  lambert0  46871  sprsymrelfolem1  47476  sprbisymrel  47483  fmtno0prm  47542  fmtno1prm  47543  fmtno2prm  47544  fmtno3prm  47546  fmtno4prm  47559  m2prm  47575  m3prm  47576  m5prm  47582  m7prm  47584  lighneallem4a  47592  0evenALTV  47672  1oddALTV  47674  2evenALTV  47676  6even  47695  7odd  47696  8even  47697  9gbo  47758  opstrgric  47910  ushggricedg  47911  grtri  47924  usgrexmpl1  48006  usgrexmpl1vtx  48007  usgrexmpl1edg  48008  usgrexmpl2  48011  usgrexmpl2vtx  48012  usgrexmpl2edg  48013  gpgprismgr4cycllem5  48083  pgnbgreunbgr  48109  pgn4cyclex  48110  uspgrex  48134  lmod1zrnlvec  48479  zlmodzxzldeplem1  48485  zlmodzxzldeplem3  48487  zlmodzxzldeplem4  48488  zlmodzxzldep  48489  ldepsnlinclem1  48490  ldepsnlinclem2  48491  blennn0elnn  48562  nn0sumshdiglemA  48604  nn0sumshdiglemB  48605  itcovalpclem2  48656  itcovalt2lem2  48661  ackval42  48681  rrx2line  48725  rrx2linesl  48728  spheres  48731  2sphere  48734  2sphere0  48735  line2x  48739  line2y  48740  resipos  48959  functhinclem1  49429  prsthinc  49449  setc1oterm  49476  funcsetc1ocl  49481  funcsetc1o  49482  isinito2lem  49483  isinito3  49485  functermc2  49494  incat  49586  setc1onsubc  49587