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 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  eqeltrri  2833  3eltr4i  2849  intab  4933  axrep6g  5235  unisn2  5257  inex2  5263  vpwex  5322  ord3ex  5332  zfpair  5366  vsnex  5379  opex  5412  otex  5413  uniopel  5464  elvvuni  5701  isarep2  6582  fvex  6847  fvexi  6848  riotaex  7319  ovexi  7392  tpex  7691  oprabex  7920  oprabrexex2  7922  mpoexw  8022  mptmpoopabbrd  8024  mptmpoopabbrdOLD  8025  tfrlem16  8324  1oex  8407  2oex  8408  1on  8409  2on  8410  3on  8413  4on  8414  oesuclem  8452  oecl  8464  o2p2e4  8468  nnecl  8541  1onnALT  8569  2onnALT  8571  3onn  8572  4onn  8573  mapsnf1o2  8832  sbthlem10  9024  cnvfi  9100  fnfi  9102  nnunifi  9191  imafiOLD  9216  pwfi  9219  prfiALT  9225  tpfi  9226  fczfsuppd  9289  cantnfvalf  9574  oemapwe  9603  cantnffval2  9604  cnfcom3clem  9614  ssttrcl  9624  r1fin  9685  hta  9809  infxpenlem  9923  alephon  9979  alephfplem1  10014  dfac5lem4  10036  dfac5lem5  10037  dfac5lem4OLD  10038  kmlem10  10070  fin1a2lem10  10319  fin1a2lem12  10321  hsmexlem9  10335  axcc2lem  10346  domtriomlem  10352  axdc2lem  10358  axcclem  10367  brdom7disj  10441  brdom6disj  10442  iundom2g  10450  konigthlem  10479  canthwelem  10561  wunex2  10649  wunex3  10652  1nq  10839  1pr  10926  nrex1  10975  axcnex  11058  ax1cn  11060  pnfex  11185  mnfxr  11189  cju  12141  nnexALT  12147  2nn  12218  2re  12219  2cn  12220  3nn  12224  3re  12225  3cn  12226  4nn  12228  4re  12229  4cn  12230  5nn  12231  5re  12232  5cn  12233  6nn  12234  6re  12235  6cn  12236  7nn  12237  7re  12238  7cn  12239  8nn  12240  8re  12241  8cn  12242  9nn  12243  9re  12244  9cn  12245  nn0ex  12407  zexALT  12508  nneo  12576  zeo  12578  deccl  12622  10re  12626  decnncl  12627  numnncl2  12630  decnncl2  12631  numsucc  12647  numma2c  12653  numadd  12654  numaddc  12655  nummul1c  12656  nummul2c  12657  decmul1  12671  qexALT  12877  xrex  12900  xnegex  13123  xnegcl  13128  ixxssxr  13273  fz0to4untppr  13546  fz0to5un2tp  13547  om2uzuzi  13872  ltweuz  13884  axdc4uzlem  13906  seqex  13926  seqexw  13940  m1expcl2  14008  faccl  14206  facwordi  14212  faclbnd2  14214  bccl  14245  hashen1  14293  hashrabrsn  14295  hashunlei  14348  hashpw  14359  tpf1o  14424  s1cli  14529  ccat2s1p1  14553  cats1un  14644  revs1  14688  cshwsexa  14747  cats1cli  14780  cats1fvn  14781  crre  15037  remim  15040  climmpt  15494  sumex  15611  supcvg  15779  geo2lim  15798  prodex  15828  bpoly4  15982  ere  16012  eftlub  16034  efsep  16035  tan0  16076  ef01bndlem  16109  nn0o  16310  divalglem5  16324  divalglem9  16328  sadcf  16380  smupf  16405  crth  16705  phimullem  16706  pczpre  16775  pockthi  16835  prmreclem2  16845  igz  16862  0ramcl  16951  1259lem1  17058  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  1259prm  17063  2503lem1  17064  2503lem2  17065  2503lem3  17066  2503prm  17067  4001lem1  17068  4001lem2  17069  4001lem3  17070  4001lem4  17071  4001prm  17072  strle1  17085  ndxarg  17123  basendxnn  17146  plusgndxnn  17205  tsetndxnn  17274  plendxnn  17288  dsndxnn  17307  unifndxnn  17317  prdsbasex  17370  prdsds  17384  yonedalem3  18203  isposix  18247  chnub  18545  plusffval  18571  issubmgm2  18628  efmnd1hash  18817  efmnd2hash  18819  smndex1bas  18831  smndex1sgrp  18833  smndex1mnd  18835  smndex1id  18836  smndex2dbas  18839  smndex2hbas  18841  grpsubfval  18913  mulgfval  18999  symg1hash  19319  symg2hash  19321  symgvalstruct  19326  symgfisg  19397  psgnsn  19449  psgnprfval1  19451  odfval  19461  sylow2alem2  19547  efgsval2  19662  efgsp1  19666  pgpfaclem1  20012  dvdsrval  20297  isirred  20355  scaffval  20831  cnfldex  21312  xrsex  21339  pzriprnglem4  21439  pzriprnglem5  21440  pzriprnglem6  21441  pzriprng1ALT  21451  znle  21491  znidomb  21516  cnmsgnsubg  21532  refld  21574  ipffval  21603  psrbag0  22017  psrbagsn  22018  psr1baslem  22125  mat1dimbas  22416  mat1dimscm  22419  mat1f1o  22422  mat1rhmelval  22424  m2detleib  22575  pmatcoe1fsupp  22645  indistopon  22945  iccordt  23158  conncompid  23375  ptbasfi  23525  ptcmpfi  23757  ustfn  24146  ust0  24164  ustn0  24165  tmslem  24426  nmfval  24532  cnbl0  24717  cnopn  24730  remet  24734  re2ndc  24745  zcld  24758  icccmp  24770  xrge0gsumle  24778  xrge0tsms  24779  xmetdcn  24783  divcnOLD  24813  divcn  24815  expcn  24819  expcnOLD  24821  iiconn  24836  idcncf  24867  cnmpopc  24878  cnrehmeo  24907  cnrehmeoOLD  24908  cnheiborlem  24909  rellycmp  24912  bndth  24913  evth2  24915  cnrlmod  25099  cnrlvec  25100  cncmet  25278  ishl2  25326  ehleudis  25374  ehleudisval  25375  finiunmbl  25501  ioombl1lem4  25518  vitalilem4  25568  vitalilem5  25569  ismbf2d  25597  mbfimaopnlem  25612  mbfi1fseqlem6  25677  itgex  25727  bddmulibl  25796  ditgex  25809  recnperf  25862  dvcnvrelem2  25979  ftc1  26005  mdegcl  26030  plyeq0lem  26171  aaliou3lem4  26310  dvradcnv  26386  sincn  26410  coscn  26411  tanabsge  26471  circsubm  26518  reloggim  26564  logcn  26612  dvloglem  26613  logdmopn  26614  dvlog2  26618  2irrexpq  26696  cxpcn  26710  cxpcnOLD  26711  cxpcn3  26714  resqrtcn  26715  2logb9irrALT  26764  2irrexpqALT  26766  atanrecl  26877  atan1  26894  atansopn  26898  birthdaylem1  26917  birthday  26920  emcllem4  26965  emcllem6  26967  lgamgulmlem6  27000  basellem6  27052  ppiublem1  27169  bposlem6  27256  bposlem8  27258  lgslem4  27267  lgsdir2lem2  27293  selberglem1  27512  selberglem3  27514  selberg  27515  selbergs  27541  qdrng  27587  0no  27805  1no  27806  lrrecse  27938  precsexlem11  28213  seqsex  28281  nnsex  28314  n0bday  28348  n0subs  28359  n0p1nns  28367  dfnns2  28368  zsex  28376  bdayfinbndlem1  28463  z12sex  28470  z12shalf  28476  edgfndxnn  29065  structvtxvallem  29093  usgrexmpllem  29333  usgrexmpl  29336  uhgrspan1  29376  upgrres  29379  umgrres  29380  usgrres  29381  upgrres1  29386  umgrres1  29387  usgrres1  29388  fusgrfis  29403  cusgrres  29522  vtxdlfgrval  29559  vtxdusgr0edgnelALT  29570  umgr2v2e  29599  vtxdginducedm1lem1  29613  vtxdginducedm1fi  29618  finsumvtxdg2ssteplem4  29622  pthdlem1  29839  crctcshlem3  29892  2wlkd  30009  2wlkond  30010  2trlond  30012  2pthd  30013  2pthond  30015  umgr2adedgwlkonALT  30020  0pth  30200  wlk2v2e  30232  3wlkd  30245  3trlond  30248  3pthd  30249  3pthond  30250  3spthond  30252  eupthvdres  30310  eulerpathpr  30315  konigsbergumgr  30326  konigsberglem5  30331  konigsberg  30332  ex-lcm  30533  isvciOLD  30655  isnvi  30688  blocni  30880  hmoval  30885  cncph  30894  ipasslem7  30911  siilem2  30927  normlem2  31186  normlem3  31187  normlem6  31190  h0elch  31330  hhssabloilem  31336  hhsssh  31344  spansnji  31721  nonbooli  31726  3oalem5  31741  3oalem6  31742  3oai  31743  mayetes3i  31804  nmcexi  32101  nmbdfnlb  32125  rnelshi  32134  cnlnadjlem5  32146  pjbdlni  32224  golem2  32347  goeqi  32348  dp2clq  32962  rpdp2cl  32963  rpdp2cl2  32964  dpmul100  32978  rpdpcl  32984  xrge0tsmsd  33155  pmtrto1cl  33181  psgnfzto1stlem  33182  fzto1st  33185  psgnfzto1st  33187  nn0omnd  33425  xrge0slmod  33429  qusima  33489  prmidl0  33531  fply1  33639  extvfvcl  33701  ply1degltdimlem  33779  ccfldextdgrr  33829  algextdeglem8  33881  constrfin  33903  2sqr3minply  33937  2sqr3nconstr  33938  cos9thpiminplylem4  33942  cos9thpiminplylem5  33943  cos9thpinconstrlem2  33947  circtopn  33994  circcn  33995  zarcmplem  34038  tpr2tp  34061  tpr2rico  34069  ordtprsval  34075  ordtprsuni  34076  ordtrestNEW  34078  ordtrest2NEWlem  34079  ordtrest2NEW  34080  ordtconnlem1  34081  mndpluscn  34083  xrge0pluscn  34097  xrge0mulc1cn  34098  xrge0haus  34101  lmlimxrge0  34105  lmxrge0  34109  qqhcn  34148  qqhucn  34149  esumex  34186  esumcst  34220  hasheuni  34242  esumcvg  34243  prsiga  34288  brsiga  34340  mbfmcnt  34425  sxbrsigalem3  34429  dya2iocuni  34440  dya2iocucvr  34441  sxbrsigalem1  34442  sxbrsiga  34447  eulerpartlemt  34528  fibp1  34558  coinflipprob  34637  coinfliprv  34640  ccatmulgnn0dir  34699  signswplusg  34712  hgt750lem2  34809  hgt750leme  34815  bnj105  34880  bnj918  34922  bnj95  35020  bnj852  35077  bnj865  35079  fineqvnttrclse  35280  subfacp1lem1  35373  subfacp1lem3  35376  subfacp1lem5  35378  subfacp1lem6  35379  kur14lem7  35406  iisconn  35446  iillysconn  35447  cvmliftlem5  35483  cvmliftlem8  35486  cvmliftlem10  35488  cvmlift2lem9  35505  satfv0  35552  goalrlem  35590  goalr  35591  satffunlem2lem2  35600  circum  35868  iexpire  35929  altopex  36154  colinearex  36254  ssoninhaus  36642  cnndvlem2  36738  bj-prex  37241  bj-prfromadj  37246  bj-pinftyccb  37426  taupi  37528  isbasisrelowl  37563  relowlpssretop  37569  poimirlem29  37850  poimirlem30  37851  poimirlem31  37852  dvasin  37905  dvacos  37906  areacirc  37914  upixp  37930  fdc  37946  lmclim2  37959  cncfres  37966  heibor1lem  38010  rrnval  38028  rrnmet  38030  reheibor  38040  isdrngo2  38159  isrngohom  38166  idlval  38214  isidl  38215  igenval  38262  scottexf  38369  cnvepresex  38529  preex  38665  renegclALT  39223  ldualfvadd  39388  cmtfvalN  39470  cvrfval  39528  cdleme31fv  40650  cdlemk40  41177  cdlemk56  41231  dibopelvalN  41403  dibopelval2  41405  dibelval3  41407  diblsmopel  41431  cdlemn11a  41467  dihopelvalcpre  41508  dihpN  41596  hlhilsca  42195  hlhilip  42208  3factsumint1  42275  lcmineqlem23  42305  aks4d1p1p6  42327  aks4d1p1p5  42329  aks6d1c6isolem2  42429  itrere  42573  acos1half  42613  redvmptabs  42615  readvrec2  42616  sn-0tie0  42706  sn-itrere  42743  sn-retire  42744  prjspval  42846  flt4lem5e  42899  sn-isghm  42916  mapfzcons2  42961  jm2.23  43238  jm2.27dlem2  43252  jm2.27dlem4  43254  rmydioph  43256  rmxdioph  43258  expdiophlem2  43264  expdioph  43265  aomclem6  43301  pwslnmlem0  43333  frlmpwfi  43340  mncn0  43381  aaitgo  43404  arearect  43457  areaquad  43458  omcl3g  43576  comptiunov2i  43947  frege110  44214  frege133  44237  scottex2  44486  radcnvrat  44555  uzmptshftfval  44587  dvradcnv2  44588  binomcxplemdvbinom  44594  binomcxplemcvg  44595  binomcxplemnotnn0  44597  permaxinf2lem  45253  rfcnpre1  45264  fcnre  45270  refsumcn  45275  refsum2cnlem1  45282  unirnmapsn  45458  infxrpnf  45690  iocopn  45766  icoopn  45771  mccl  45844  clim1fr1  45847  islptre  45865  sumnnodd  45876  lptre2pt  45884  limclner  45895  limclr  45899  expfac  45901  0cnf  46121  icccncfext  46131  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  itgsin0pilem1  46194  iblempty  46209  itgvol0  46212  stoweidlem47  46291  stoweidlem53  46297  stoweidlem57  46301  stoweidlem59  46303  wallispilem3  46311  wallispilem4  46312  wallispilem5  46313  wallispi  46314  stirlinglem1  46318  stirlinglem8  46325  stirlinglem12  46329  stirlinglem13  46330  stirlinglem14  46331  stirlinglem15  46332  dirkerper  46340  dirkercncflem2  46348  fourierdlem16  46367  fourierdlem21  46372  fourierdlem22  46373  fourierdlem36  46387  fourierdlem42  46393  fourierdlem71  46421  fourierdlem83  46433  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem111  46461  fourierdlem112  46462  fourierdlem114  46464  sqwvfoura  46472  sqwvfourb  46473  fourierswlem  46474  fouriersw  46475  etransclem48  46526  salexct3  46586  salgencntex  46587  salgensscntex  46588  iooborel  46595  bor1sal  46599  gsumge0cl  46615  sge0tsms  46624  sge0isum  46671  nnfoctbdjlem  46699  isomenndlem  46774  mbfresmf  46983  incsmflem  46985  incsmf  46986  smfmbfcex  47004  decsmflem  47010  decsmf  47011  smflimlem1  47015  smfpimbor1lem2  47043  smf2id  47045  smfco  47046  smfpimcclem  47051  lambert0  47133  sprsymrelfolem1  47738  sprbisymrel  47745  fmtno0prm  47804  fmtno1prm  47805  fmtno2prm  47806  fmtno3prm  47808  fmtno4prm  47821  m2prm  47837  m3prm  47838  m5prm  47844  m7prm  47846  lighneallem4a  47854  0evenALTV  47934  1oddALTV  47936  2evenALTV  47938  6even  47957  7odd  47958  8even  47959  9gbo  48020  opstrgric  48172  ushggricedg  48173  grtri  48186  usgrexmpl1  48268  usgrexmpl1vtx  48269  usgrexmpl1edg  48270  usgrexmpl2  48273  usgrexmpl2vtx  48274  usgrexmpl2edg  48275  gpgprismgr4cycllem5  48345  pgnbgreunbgr  48371  pgn4cyclex  48372  uspgrex  48396  lmod1zrnlvec  48740  zlmodzxzldeplem1  48746  zlmodzxzldeplem3  48748  zlmodzxzldeplem4  48749  zlmodzxzldep  48750  ldepsnlinclem1  48751  ldepsnlinclem2  48752  blennn0elnn  48823  nn0sumshdiglemA  48865  nn0sumshdiglemB  48866  itcovalpclem2  48917  itcovalt2lem2  48922  ackval42  48942  rrx2line  48986  rrx2linesl  48989  spheres  48992  2sphere  48995  2sphere0  48996  line2x  49000  line2y  49001  resipos  49220  functhinclem1  49689  prsthinc  49709  setc1oterm  49736  funcsetc1ocl  49741  funcsetc1o  49742  isinito2lem  49743  isinito3  49745  functermc2  49754  incat  49846  setc1onsubc  49847