Theorem eqeltri 2825

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 2820	. 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 2702

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

This theorem is referenced by:  eqeltrri  2826  3eltr4i  2842  intab  4945  axrep6g  5248  unisn2  5270  inex2  5276  vpwex  5335  ord3ex  5345  zfpair  5379  vsnex  5392  opex  5427  otex  5428  uniopel  5479  elvvuni  5718  isarep2  6611  fvex  6874  fvexi  6875  riotaex  7351  ovexi  7424  tpex  7725  oprabex  7958  oprabrexex2  7960  mpoexw  8060  mptmpoopabbrd  8062  mptmpoopabbrdOLD  8063  tfrlem16  8364  1oex  8447  2oex  8448  1on  8449  2on  8450  3on  8453  4on  8454  oesuclem  8492  oecl  8504  o2p2e4  8508  nnecl  8580  1onnALT  8608  2onnALT  8610  3onn  8611  4onn  8612  mapsnf1o2  8870  sbthlem10  9066  cnvfi  9146  fnfi  9148  nnunifi  9245  imafiOLD  9272  pwfi  9275  xpfiOLD  9277  prfiALT  9282  tpfi  9283  fczfsuppd  9344  cantnfvalf  9625  oemapwe  9654  cantnffval2  9655  cnfcom3clem  9665  ssttrcl  9675  r1fin  9733  hta  9857  infxpenlem  9973  alephon  10029  alephfplem1  10064  dfac5lem4  10086  dfac5lem5  10087  dfac5lem4OLD  10088  kmlem10  10120  fin1a2lem10  10369  fin1a2lem12  10371  hsmexlem9  10385  axcc2lem  10396  domtriomlem  10402  axdc2lem  10408  axcclem  10417  brdom7disj  10491  brdom6disj  10492  iundom2g  10500  konigthlem  10528  canthwelem  10610  wunex2  10698  wunex3  10701  1nq  10888  1pr  10975  nrex1  11024  axcnex  11107  ax1cn  11109  pnfex  11234  mnfxr  11238  cju  12189  nnexALT  12195  2nn  12266  2re  12267  2cn  12268  3nn  12272  3re  12273  3cn  12274  4nn  12276  4re  12277  4cn  12278  5nn  12279  5re  12280  5cn  12281  6nn  12282  6re  12283  6cn  12284  7nn  12285  7re  12286  7cn  12287  8nn  12288  8re  12289  8cn  12290  9nn  12291  9re  12292  9cn  12293  nn0ex  12455  zexALT  12556  nneo  12625  zeo  12627  deccl  12671  10re  12675  decnncl  12676  numnncl2  12679  decnncl2  12680  numsucc  12696  numma2c  12702  numadd  12703  numaddc  12704  nummul1c  12705  nummul2c  12706  decmul1  12720  qexALT  12930  xrex  12953  xnegex  13175  xnegcl  13180  ixxssxr  13325  fz0to4untppr  13598  fz0to5un2tp  13599  om2uzuzi  13921  ltweuz  13933  axdc4uzlem  13955  seqex  13975  seqexw  13989  m1expcl2  14057  faccl  14255  facwordi  14261  faclbnd2  14263  bccl  14294  hashen1  14342  hashrabrsn  14344  hashunlei  14397  hashpw  14408  tpf1o  14473  s1cli  14577  ccat2s1p1  14601  cats1un  14693  revs1  14737  cshwsexa  14796  cshwsexaOLD  14797  cats1cli  14830  cats1fvn  14831  crre  15087  remim  15090  climmpt  15544  sumex  15661  supcvg  15829  geo2lim  15848  prodex  15878  bpoly4  16032  ere  16062  eftlub  16084  efsep  16085  tan0  16126  ef01bndlem  16159  nn0o  16360  divalglem5  16374  divalglem9  16378  sadcf  16430  smupf  16455  crth  16755  phimullem  16756  pczpre  16825  pockthi  16885  prmreclem2  16895  igz  16912  0ramcl  17001  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  1259prm  17113  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  4001prm  17122  strle1  17135  ndxarg  17173  basendxnn  17196  plusgndxnn  17255  tsetndxnn  17324  plendxnn  17338  dsndxnn  17357  unifndxnn  17367  prdsbasex  17420  prdsds  17434  yonedalem3  18248  isposix  18292  plusffval  18580  issubmgm2  18637  efmnd1hash  18826  efmnd2hash  18828  smndex1bas  18840  smndex1sgrp  18842  smndex1mnd  18844  smndex1id  18845  smndex2dbas  18848  smndex2hbas  18850  grpsubfval  18922  mulgfval  19008  symg1hash  19327  symg2hash  19329  symgvalstruct  19334  symgfisg  19405  psgnsn  19457  psgnprfval1  19459  odfval  19469  sylow2alem2  19555  efgsval2  19670  efgsp1  19674  pgpfaclem1  20020  dvdsrval  20277  isirred  20335  scaffval  20793  cnfldex  21274  xrsex  21301  pzriprnglem4  21401  pzriprnglem5  21402  pzriprnglem6  21403  pzriprng1ALT  21413  znle  21453  znidomb  21478  cnmsgnsubg  21493  refld  21535  ipffval  21564  psrbag0  21976  psrbagsn  21977  psr1baslem  22076  mat1dimbas  22366  mat1dimscm  22369  mat1f1o  22372  mat1rhmelval  22374  m2detleib  22525  pmatcoe1fsupp  22595  indistopon  22895  iccordt  23108  conncompid  23325  ptbasfi  23475  ptcmpfi  23707  ustfn  24096  ust0  24114  ustn0  24115  tmslem  24377  nmfval  24483  cnbl0  24668  cnopn  24681  remet  24685  re2ndc  24696  zcld  24709  icccmp  24721  xrge0gsumle  24729  xrge0tsms  24730  xmetdcn  24734  divcnOLD  24764  divcn  24766  expcn  24770  expcnOLD  24772  iiconn  24787  idcncf  24818  cnmpopc  24829  cnrehmeo  24858  cnrehmeoOLD  24859  cnheiborlem  24860  rellycmp  24863  bndth  24864  evth2  24866  cnrlmod  25050  cnrlvec  25051  cncmet  25229  ishl2  25277  ehleudis  25325  ehleudisval  25326  finiunmbl  25452  ioombl1lem4  25469  vitalilem4  25519  vitalilem5  25520  ismbf2d  25548  mbfimaopnlem  25563  mbfi1fseqlem6  25628  itgex  25678  bddmulibl  25747  ditgex  25760  recnperf  25813  dvcnvrelem2  25930  ftc1  25956  mdegcl  25981  plyeq0lem  26122  aaliou3lem4  26261  dvradcnv  26337  sincn  26361  coscn  26362  tanabsge  26422  circsubm  26469  reloggim  26515  logcn  26563  dvloglem  26564  logdmopn  26565  dvlog2  26569  2irrexpq  26647  cxpcn  26661  cxpcnOLD  26662  cxpcn3  26665  resqrtcn  26666  2logb9irrALT  26715  2irrexpqALT  26717  atanrecl  26828  atan1  26845  atansopn  26849  birthdaylem1  26868  birthday  26871  emcllem4  26916  emcllem6  26918  lgamgulmlem6  26951  basellem6  27003  ppiublem1  27120  bposlem6  27207  bposlem8  27209  lgslem4  27218  lgsdir2lem2  27244  selberglem1  27463  selberglem3  27465  selberg  27466  selbergs  27492  qdrng  27538  0sno  27745  1sno  27746  lrrecse  27856  precsexlem11  28126  seqsex  28186  nnsex  28218  n0sbday  28251  n0subs  28260  n0p1nns  28267  dfnns2  28268  zsex  28275  zs12ex  28345  edgfndxnn  28926  structvtxvallem  28954  usgrexmpllem  29194  usgrexmpl  29197  uhgrspan1  29237  upgrres  29240  umgrres  29241  usgrres  29242  upgrres1  29247  umgrres1  29248  usgrres1  29249  fusgrfis  29264  cusgrres  29383  vtxdlfgrval  29420  vtxdusgr0edgnelALT  29431  umgr2v2e  29460  vtxdginducedm1lem1  29474  vtxdginducedm1fi  29479  finsumvtxdg2ssteplem4  29483  pthdlem1  29703  crctcshlem3  29756  2wlkd  29873  2wlkond  29874  2trlond  29876  2pthd  29877  2pthond  29879  umgr2adedgwlkonALT  29884  0pth  30061  wlk2v2e  30093  3wlkd  30106  3trlond  30109  3pthd  30110  3pthond  30111  3spthond  30113  eupthvdres  30171  eulerpathpr  30176  konigsbergumgr  30187  konigsberglem5  30192  konigsberg  30193  ex-lcm  30394  isvciOLD  30516  isnvi  30549  blocni  30741  hmoval  30746  cncph  30755  ipasslem7  30772  siilem2  30788  normlem2  31047  normlem3  31048  normlem6  31051  h0elch  31191  hhssabloilem  31197  hhsssh  31205  spansnji  31582  nonbooli  31587  3oalem5  31602  3oalem6  31603  3oai  31604  mayetes3i  31665  nmcexi  31962  nmbdfnlb  31986  rnelshi  31995  cnlnadjlem5  32007  pjbdlni  32085  golem2  32208  goeqi  32209  dp2clq  32808  rpdp2cl  32809  rpdp2cl2  32810  dpmul100  32824  rpdpcl  32830  chnub  32945  xrge0tsmsd  33009  pmtrto1cl  33063  psgnfzto1stlem  33064  fzto1st  33067  psgnfzto1st  33069  nn0omnd  33323  xrge0slmod  33326  qusima  33386  prmidl0  33428  fply1  33534  ply1degltdimlem  33625  ccfldextdgrr  33674  algextdeglem8  33721  constrfin  33743  2sqr3minply  33777  2sqr3nconstr  33778  cos9thpiminplylem4  33782  cos9thpiminplylem5  33783  cos9thpinconstrlem2  33787  circtopn  33834  circcn  33835  zarcmplem  33878  tpr2tp  33901  tpr2rico  33909  ordtprsval  33915  ordtprsuni  33916  ordtrestNEW  33918  ordtrest2NEWlem  33919  ordtrest2NEW  33920  ordtconnlem1  33921  mndpluscn  33923  xrge0pluscn  33937  xrge0mulc1cn  33938  xrge0haus  33941  lmlimxrge0  33945  lmxrge0  33949  qqhcn  33988  qqhucn  33989  esumex  34026  esumcst  34060  hasheuni  34082  esumcvg  34083  prsiga  34128  brsiga  34180  mbfmcnt  34266  sxbrsigalem3  34270  dya2iocuni  34281  dya2iocucvr  34282  sxbrsigalem1  34283  sxbrsiga  34288  eulerpartlemt  34369  fibp1  34399  coinflipprob  34478  coinfliprv  34481  ccatmulgnn0dir  34540  signswplusg  34553  hgt750lem2  34650  hgt750leme  34656  bnj105  34721  bnj918  34763  bnj95  34861  bnj852  34918  bnj865  34920  subfacp1lem1  35173  subfacp1lem3  35176  subfacp1lem5  35178  subfacp1lem6  35179  kur14lem7  35206  iisconn  35246  iillysconn  35247  cvmliftlem5  35283  cvmliftlem8  35286  cvmliftlem10  35288  cvmlift2lem9  35305  satfv0  35352  goalrlem  35390  goalr  35391  satffunlem2lem2  35400  circum  35668  iexpire  35729  altopex  35955  colinearex  36055  ssoninhaus  36443  cnndvlem2  36533  bj-prex  37035  bj-prfromadj  37040  bj-pinftyccb  37216  taupi  37318  isbasisrelowl  37353  relowlpssretop  37359  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  dvasin  37705  dvacos  37706  areacirc  37714  upixp  37730  fdc  37746  lmclim2  37759  cncfres  37766  heibor1lem  37810  rrnval  37828  rrnmet  37830  reheibor  37840  isdrngo2  37959  isrngohom  37966  idlval  38014  isidl  38015  igenval  38062  scottexf  38169  cnvepresex  38325  renegclALT  38963  ldualfvadd  39128  cmtfvalN  39210  cvrfval  39268  cdleme31fv  40391  cdlemk40  40918  cdlemk56  40972  dibopelvalN  41144  dibopelval2  41146  dibelval3  41148  diblsmopel  41172  cdlemn11a  41208  dihopelvalcpre  41249  dihpN  41337  hlhilsca  41936  hlhilip  41949  3factsumint1  42016  lcmineqlem23  42046  aks4d1p1p6  42068  aks4d1p1p5  42070  aks6d1c6isolem2  42170  itrere  42313  acos1half  42353  redvmptabs  42355  readvrec2  42356  sn-0tie0  42446  sn-itrere  42483  sn-retire  42484  prjspval  42598  flt4lem5e  42651  sn-isghm  42668  mapfzcons2  42714  jm2.23  42992  jm2.27dlem2  43006  jm2.27dlem4  43008  rmydioph  43010  rmxdioph  43012  expdiophlem2  43018  expdioph  43019  aomclem6  43055  pwslnmlem0  43087  frlmpwfi  43094  mncn0  43135  aaitgo  43158  arearect  43211  areaquad  43212  omcl3g  43330  comptiunov2i  43702  frege110  43969  frege133  43992  scottex2  44241  radcnvrat  44310  uzmptshftfval  44342  dvradcnv2  44343  binomcxplemdvbinom  44349  binomcxplemcvg  44350  binomcxplemnotnn0  44352  permaxinf2lem  45009  rfcnpre1  45020  fcnre  45026  refsumcn  45031  refsum2cnlem1  45038  unirnmapsn  45215  infxrpnf  45449  iocopn  45525  icoopn  45530  mccl  45603  clim1fr1  45606  islptre  45624  sumnnodd  45635  lptre2pt  45645  limclner  45656  limclr  45660  expfac  45662  0cnf  45882  icccncfext  45892  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  itgsin0pilem1  45955  iblempty  45970  itgvol0  45973  stoweidlem47  46052  stoweidlem53  46058  stoweidlem57  46062  stoweidlem59  46064  wallispilem3  46072  wallispilem4  46073  wallispilem5  46074  wallispi  46075  stirlinglem1  46079  stirlinglem8  46086  stirlinglem12  46090  stirlinglem13  46091  stirlinglem14  46092  stirlinglem15  46093  dirkerper  46101  dirkercncflem2  46109  fourierdlem16  46128  fourierdlem21  46133  fourierdlem22  46134  fourierdlem36  46148  fourierdlem42  46154  fourierdlem71  46182  fourierdlem83  46194  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem112  46223  fourierdlem114  46225  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  etransclem48  46287  salexct3  46347  salgencntex  46348  salgensscntex  46349  iooborel  46356  bor1sal  46360  gsumge0cl  46376  sge0tsms  46385  sge0isum  46432  nnfoctbdjlem  46460  isomenndlem  46535  mbfresmf  46744  incsmflem  46746  incsmf  46747  smfmbfcex  46765  decsmflem  46771  decsmf  46772  smflimlem1  46776  smfpimbor1lem2  46804  smf2id  46806  smfco  46807  smfpimcclem  46812  tworepnotupword  46891  lambert0  46895  sprsymrelfolem1  47497  sprbisymrel  47504  fmtno0prm  47563  fmtno1prm  47564  fmtno2prm  47565  fmtno3prm  47567  fmtno4prm  47580  m2prm  47596  m3prm  47597  m5prm  47603  m7prm  47605  lighneallem4a  47613  0evenALTV  47693  1oddALTV  47695  2evenALTV  47697  6even  47716  7odd  47717  8even  47718  9gbo  47779  opstrgric  47930  ushggricedg  47931  grtri  47943  usgrexmpl1  48017  usgrexmpl1vtx  48018  usgrexmpl1edg  48019  usgrexmpl2  48022  usgrexmpl2vtx  48023  usgrexmpl2edg  48024  gpgprismgr4cycllem5  48093  pgnbgreunbgr  48119  pgn4cyclex  48120  uspgrex  48142  lmod1zrnlvec  48487  zlmodzxzldeplem1  48493  zlmodzxzldeplem3  48495  zlmodzxzldeplem4  48496  zlmodzxzldep  48497  ldepsnlinclem1  48498  ldepsnlinclem2  48499  blennn0elnn  48570  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  itcovalpclem2  48664  itcovalt2lem2  48669  ackval42  48689  rrx2line  48733  rrx2linesl  48736  spheres  48739  2sphere  48742  2sphere0  48743  line2x  48747  line2y  48748  resipos  48967  functhinclem1  49437  prsthinc  49457  setc1oterm  49484  funcsetc1ocl  49489  funcsetc1o  49490  isinito2lem  49491  isinito3  49493  functermc2  49502  incat  49594  setc1onsubc  49595