Theorem eqeltri 2832

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

Syntax hints:   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811

This theorem is referenced by:  eqeltrri  2833  3eltr4i  2849  intab  4920  axrep6g  5225  unisn2  5247  inex2  5259  vpwex  5319  ord3ex  5329  zfpair  5363  vsnex  5377  snex  5381  opex  5416  opexOLD  5417  otex  5418  uniopel  5470  elvvuni  5708  isarep2  6588  fvex  6853  fvexi  6854  riotaex  7328  ovexi  7401  tpex  7700  oprabex  7929  oprabrexex2  7931  mpoexw  8031  mptmpoopabbrd  8033  tfrlem16  8332  1oex  8415  2oex  8416  1on  8417  2on  8418  3on  8421  4on  8422  oesuclem  8460  oecl  8472  o2p2e4  8476  nnecl  8549  1onnALT  8577  2onnALT  8579  3onn  8580  4onn  8581  mapsnf1o2  8842  sbthlem10  9034  cnvfi  9110  fnfi  9112  nnunifi  9201  imafiOLD  9226  pwfi  9229  prfiALT  9235  tpfi  9236  fczfsuppd  9299  cantnfvalf  9586  oemapwe  9615  cantnffval2  9616  cnfcom3clem  9626  ssttrcl  9636  r1fin  9697  hta  9821  infxpenlem  9935  alephon  9991  alephfplem1  10026  dfac5lem4  10048  dfac5lem5  10049  dfac5lem4OLD  10050  kmlem10  10082  fin1a2lem10  10331  fin1a2lem12  10333  hsmexlem9  10347  axcc2lem  10358  domtriomlem  10364  axdc2lem  10370  axcclem  10379  brdom7disj  10453  brdom6disj  10454  iundom2g  10462  konigthlem  10491  canthwelem  10573  wunex2  10661  wunex3  10664  1nq  10851  1pr  10938  nrex1  10987  axcnex  11070  ax1cn  11072  pnfex  11198  mnfxr  11202  cju  12155  nnexALT  12176  2nn  12254  2re  12255  2cn  12256  3nn  12260  3re  12261  3cn  12262  4nn  12264  4re  12265  4cn  12266  5nn  12267  5re  12268  5cn  12269  6nn  12270  6re  12271  6cn  12272  7nn  12273  7re  12274  7cn  12275  8nn  12276  8re  12277  8cn  12278  9nn  12279  9re  12280  9cn  12281  nn0ex  12443  zexALT  12544  nneo  12613  zeo  12615  deccl  12659  10re  12663  decnncl  12664  numnncl2  12667  decnncl2  12668  numsucc  12684  numma2c  12690  numadd  12691  numaddc  12692  nummul1c  12693  nummul2c  12694  decmul1  12708  qexALT  12914  xrex  12937  xnegex  13160  xnegcl  13165  ixxssxr  13310  fz0to4untppr  13584  fz0to5un2tp  13585  om2uzuzi  13911  ltweuz  13923  axdc4uzlem  13945  seqex  13965  seqexw  13979  m1expcl2  14047  faccl  14245  facwordi  14251  faclbnd2  14253  bccl  14284  hashen1  14332  hashrabrsn  14334  hashunlei  14387  hashpw  14398  tpf1o  14463  s1cli  14568  ccat2s1p1  14592  cats1un  14683  revs1  14727  cshwsexa  14786  cats1cli  14819  cats1fvn  14820  crre  15076  remim  15079  climmpt  15533  sumex  15650  supcvg  15821  geo2lim  15840  prodex  15870  bpoly4  16024  ere  16054  eftlub  16076  efsep  16077  tan0  16118  ef01bndlem  16151  nn0o  16352  divalglem5  16366  divalglem9  16370  sadcf  16422  smupf  16447  crth  16748  phimullem  16749  pczpre  16818  pockthi  16878  prmreclem2  16888  igz  16905  0ramcl  16994  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  strle1  17128  ndxarg  17166  basendxnn  17189  plusgndxnn  17248  tsetndxnn  17317  plendxnn  17331  dsndxnn  17350  unifndxnn  17360  prdsbasex  17413  prdsds  17427  yonedalem3  18246  isposix  18290  chnub  18588  plusffval  18614  issubmgm2  18671  efmnd1hash  18860  efmnd2hash  18862  smndex1bas  18877  smndex1sgrp  18879  smndex1mnd  18881  smndex1id  18882  smndex2dbas  18885  smndex2hbas  18887  grpsubfval  18959  mulgfval  19045  symg1hash  19365  symg2hash  19367  symgvalstruct  19372  symgfisg  19443  psgnsn  19495  psgnprfval1  19497  odfval  19507  sylow2alem2  19593  efgsval2  19708  efgsp1  19712  pgpfaclem1  20058  dvdsrval  20341  isirred  20399  scaffval  20875  cnfldex  21355  xrsex  21369  pzriprnglem4  21464  pzriprnglem5  21465  pzriprnglem6  21466  pzriprng1ALT  21476  znle  21516  znidomb  21541  cnmsgnsubg  21557  refld  21599  ipffval  21628  psrbag0  22040  psrbagsn  22041  psr1baslem  22148  mat1dimbas  22437  mat1dimscm  22440  mat1f1o  22443  mat1rhmelval  22445  m2detleib  22596  pmatcoe1fsupp  22666  indistopon  22966  iccordt  23179  conncompid  23396  ptbasfi  23546  ptcmpfi  23778  ustfn  24167  ust0  24185  ustn0  24186  tmslem  24447  nmfval  24553  cnbl0  24738  cnopn  24751  remet  24755  re2ndc  24766  zcld  24779  icccmp  24791  xrge0gsumle  24799  xrge0tsms  24800  xmetdcn  24804  divcn  24835  expcn  24839  iiconn  24854  idcncf  24885  cnmpopc  24895  cnrehmeo  24920  cnheiborlem  24921  rellycmp  24924  bndth  24925  evth2  24927  cnrlmod  25110  cnrlvec  25111  cncmet  25289  ishl2  25337  ehleudis  25385  ehleudisval  25386  finiunmbl  25511  ioombl1lem4  25528  vitalilem4  25578  vitalilem5  25579  ismbf2d  25607  mbfimaopnlem  25622  mbfi1fseqlem6  25687  itgex  25737  bddmulibl  25806  ditgex  25819  recnperf  25872  dvcnvrelem2  25985  ftc1  26009  mdegcl  26034  plyeq0lem  26175  aaliou3lem4  26312  dvradcnv  26386  sincn  26409  coscn  26410  tanabsge  26470  circsubm  26517  reloggim  26563  logcn  26611  dvloglem  26612  logdmopn  26613  dvlog2  26617  2irrexpq  26695  cxpcn  26709  cxpcn3  26712  resqrtcn  26713  2logb9irrALT  26762  2irrexpqALT  26764  atanrecl  26875  atan1  26892  atansopn  26896  birthdaylem1  26915  birthday  26918  emcllem4  26962  emcllem6  26964  lgamgulmlem6  26997  basellem6  27049  ppiublem1  27165  bposlem6  27252  bposlem8  27254  lgslem4  27263  lgsdir2lem2  27289  selberglem1  27508  selberglem3  27510  selberg  27511  selbergs  27537  qdrng  27583  0no  27801  1no  27802  lrrecse  27934  precsexlem11  28209  seqsex  28277  nnsex  28310  n0bday  28344  n0subs  28355  n0p1nns  28363  dfnns2  28364  zsex  28372  bdayfinbndlem1  28459  z12sex  28466  z12shalf  28472  edgfndxnn  29061  structvtxvallem  29089  usgrexmpllem  29329  usgrexmpl  29332  uhgrspan1  29372  upgrres  29375  umgrres  29376  usgrres  29377  upgrres1  29382  umgrres1  29383  usgrres1  29384  fusgrfis  29399  cusgrres  29517  vtxdlfgrval  29554  vtxdusgr0edgnelALT  29565  umgr2v2e  29594  vtxdginducedm1lem1  29608  vtxdginducedm1fi  29613  finsumvtxdg2ssteplem4  29617  pthdlem1  29834  crctcshlem3  29887  2wlkd  30004  2wlkond  30005  2trlond  30007  2pthd  30008  2pthond  30010  umgr2adedgwlkonALT  30015  0pth  30195  wlk2v2e  30227  3wlkd  30240  3trlond  30243  3pthd  30244  3pthond  30245  3spthond  30247  eupthvdres  30305  eulerpathpr  30310  konigsbergumgr  30321  konigsberglem5  30326  konigsberg  30327  ex-lcm  30528  isvciOLD  30651  isnvi  30684  blocni  30876  hmoval  30881  cncph  30890  ipasslem7  30907  siilem2  30923  normlem2  31182  normlem3  31183  normlem6  31186  h0elch  31326  hhssabloilem  31332  hhsssh  31340  spansnji  31717  nonbooli  31722  3oalem5  31737  3oalem6  31738  3oai  31739  mayetes3i  31800  nmcexi  32097  nmbdfnlb  32121  rnelshi  32130  cnlnadjlem5  32142  pjbdlni  32220  golem2  32343  goeqi  32344  dp2clq  32940  rpdp2cl  32941  rpdp2cl2  32942  dpmul100  32956  rpdpcl  32962  xrge0tsmsd  33134  pmtrto1cl  33160  psgnfzto1stlem  33161  fzto1st  33164  psgnfzto1st  33166  nn0omnd  33404  xrge0slmod  33408  qusima  33468  prmidl0  33510  fply1  33618  extvfvcl  33680  ply1degltdimlem  33766  ccfldextdgrr  33816  algextdeglem8  33868  constrfin  33890  2sqr3minply  33924  2sqr3nconstr  33925  cos9thpiminplylem4  33929  cos9thpiminplylem5  33930  cos9thpinconstrlem2  33934  circtopn  33981  circcn  33982  zarcmplem  34025  tpr2tp  34048  tpr2rico  34056  ordtprsval  34062  ordtprsuni  34063  ordtrestNEW  34065  ordtrest2NEWlem  34066  ordtrest2NEW  34067  ordtconnlem1  34068  mndpluscn  34070  xrge0pluscn  34084  xrge0mulc1cn  34085  xrge0haus  34088  lmlimxrge0  34092  lmxrge0  34096  qqhcn  34135  qqhucn  34136  esumex  34173  esumcst  34207  hasheuni  34229  esumcvg  34230  prsiga  34275  brsiga  34327  mbfmcnt  34412  sxbrsigalem3  34416  dya2iocuni  34427  dya2iocucvr  34428  sxbrsigalem1  34429  sxbrsiga  34434  eulerpartlemt  34515  fibp1  34545  coinflipprob  34624  coinfliprv  34627  ccatmulgnn0dir  34686  signswplusg  34699  hgt750lem2  34796  hgt750leme  34802  bnj105  34867  bnj918  34909  bnj95  35006  bnj852  35063  bnj865  35065  fineqvnttrclse  35268  subfacp1lem1  35361  subfacp1lem3  35364  subfacp1lem5  35366  subfacp1lem6  35367  kur14lem7  35394  iisconn  35434  iillysconn  35435  cvmliftlem5  35471  cvmliftlem8  35474  cvmliftlem10  35476  cvmlift2lem9  35493  satfv0  35540  goalrlem  35578  goalr  35579  satffunlem2lem2  35588  circum  35856  iexpire  35917  altopex  36142  colinearex  36242  ssoninhaus  36630  cnndvlem2  36798  bj-prex  37347  bj-prfromadj  37352  bj-pinftyccb  37535  taupi  37637  isbasisrelowl  37674  relowlpssretop  37680  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  dvasin  38025  dvacos  38026  areacirc  38034  upixp  38050  fdc  38066  lmclim2  38079  cncfres  38086  heibor1lem  38130  rrnval  38148  rrnmet  38150  reheibor  38160  isdrngo2  38279  isrngohom  38286  idlval  38334  isidl  38335  igenval  38382  scottexf  38489  cnvepresex  38657  preex  38813  renegclALT  39409  ldualfvadd  39574  cmtfvalN  39656  cvrfval  39714  cdleme31fv  40836  cdlemk40  41363  cdlemk56  41417  dibopelvalN  41589  dibopelval2  41591  dibelval3  41593  diblsmopel  41617  cdlemn11a  41653  dihopelvalcpre  41694  dihpN  41782  hlhilsca  42381  hlhilip  42394  3factsumint1  42460  lcmineqlem23  42490  aks4d1p1p6  42512  aks4d1p1p5  42514  aks6d1c6isolem2  42614  itrere  42750  acos1half  42790  redvmptabs  42792  readvrec2  42793  sn-0tie0  42896  sn-itrere  42933  sn-retire  42934  prjspval  43036  flt4lem5e  43089  sn-isghm  43106  mapfzcons2  43151  jm2.23  43424  jm2.27dlem2  43438  jm2.27dlem4  43440  rmydioph  43442  rmxdioph  43444  expdiophlem2  43450  expdioph  43451  aomclem6  43487  pwslnmlem0  43519  frlmpwfi  43526  mncn0  43567  aaitgo  43590  arearect  43643  areaquad  43644  omcl3g  43762  comptiunov2i  44133  frege110  44400  frege133  44423  scottex2  44672  radcnvrat  44741  uzmptshftfval  44773  dvradcnv2  44774  binomcxplemdvbinom  44780  binomcxplemcvg  44781  binomcxplemnotnn0  44783  permaxinf2lem  45439  rfcnpre1  45450  fcnre  45456  refsumcn  45461  refsum2cnlem1  45468  unirnmapsn  45643  infxrpnf  45874  iocopn  45950  icoopn  45955  mccl  46028  clim1fr1  46031  islptre  46049  sumnnodd  46060  lptre2pt  46068  limclner  46079  limclr  46083  expfac  46085  0cnf  46305  icccncfext  46315  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  itgsin0pilem1  46378  iblempty  46393  itgvol0  46396  stoweidlem47  46475  stoweidlem53  46481  stoweidlem57  46485  stoweidlem59  46487  wallispilem3  46495  wallispilem4  46496  wallispilem5  46497  wallispi  46498  stirlinglem1  46502  stirlinglem8  46509  stirlinglem12  46513  stirlinglem13  46514  stirlinglem14  46515  stirlinglem15  46516  dirkerper  46524  dirkercncflem2  46532  fourierdlem16  46551  fourierdlem21  46556  fourierdlem22  46557  fourierdlem36  46571  fourierdlem42  46577  fourierdlem71  46605  fourierdlem83  46617  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  fourierdlem114  46648  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  etransclem48  46710  salexct3  46770  salgencntex  46771  salgensscntex  46772  iooborel  46779  bor1sal  46783  gsumge0cl  46799  sge0tsms  46808  sge0isum  46855  nnfoctbdjlem  46883  isomenndlem  46958  mbfresmf  47167  incsmflem  47169  incsmf  47170  smfmbfcex  47188  decsmflem  47194  decsmf  47195  smflimlem1  47199  smfpimbor1lem2  47227  smf2id  47229  smfco  47230  smfpimcclem  47235  goldrarr  47329  lambert0  47335  sprsymrelfolem1  47952  sprbisymrel  47959  fmtno0prm  48021  fmtno1prm  48022  fmtno2prm  48023  fmtno3prm  48025  fmtno4prm  48038  m2prm  48054  m3prm  48055  m5prm  48061  m7prm  48063  lighneallem4a  48071  nprmdvdsfacm1lem4  48086  0evenALTV  48164  1oddALTV  48166  2evenALTV  48168  6even  48187  7odd  48188  8even  48189  9gbo  48250  opstrgric  48402  ushggricedg  48403  grtri  48416  usgrexmpl1  48498  usgrexmpl1vtx  48499  usgrexmpl1edg  48500  usgrexmpl2  48503  usgrexmpl2vtx  48504  usgrexmpl2edg  48505  gpgprismgr4cycllem5  48575  pgnbgreunbgr  48601  pgn4cyclex  48602  uspgrex  48626  lmod1zrnlvec  48970  zlmodzxzldeplem1  48976  zlmodzxzldeplem3  48978  zlmodzxzldeplem4  48979  zlmodzxzldep  48980  ldepsnlinclem1  48981  ldepsnlinclem2  48982  blennn0elnn  49053  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  itcovalpclem2  49147  itcovalt2lem2  49152  ackval42  49172  rrx2line  49216  rrx2linesl  49219  spheres  49222  2sphere  49225  2sphere0  49226  line2x  49230  line2y  49231  resipos  49450  functhinclem1  49919  prsthinc  49939  setc1oterm  49966  funcsetc1ocl  49971  funcsetc1o  49972  isinito2lem  49973  isinito3  49975  functermc2  49984  incat  50076  setc1onsubc  50077