Theorem eqeltri 2865

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

Syntax hints:   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  eqeltrri  2866  3eltr4i  2882  intab  4947  axrep6g  5255  unisn2  5277  inex2  5289  vpwex  5349  ord3ex  5359  zfpair  5393  vsnex  5407  snex  5411  opex  5446  opexOLD  5447  otex  5448  uniopel  5500  elvvuni  5739  isarep2  6626  fvex  6895  fvexi  6896  riotaex  7372  ovexi  7445  tpex  7744  oprabex  7972  oprabrexex2  7974  mpoexw  8074  mptmpoopabbrd  8077  tfrlem16  8379  1oex  8462  2oex  8464  1on  8465  2on  8466  3on  8469  4on  8470  oesuclem  8509  oecl  8521  o2p2e4  8525  nnecl  8598  1onnALT  8626  2onnALT  8628  3onn  8629  4onn  8630  mapsnf1o2  8891  sbthlem10  9083  cnvfi  9159  fnfi  9161  nnunifi  9250  pwfi  9277  prfiALT  9283  tpfi  9284  fczfsuppd  9345  cantnfvalf  9633  oemapwe  9662  cantnffval2  9663  cnfcom3clem  9673  ssttrcl  9683  r1fin  9744  scottex2  9870  hta  9882  infxpenlem  9996  alephon  10052  alephfplem1  10087  dfac5lem4  10109  dfac5lem5  10110  kmlem10  10142  fin1a2lem10  10392  fin1a2lem12  10394  hsmexlem9  10408  axcc2lem  10419  domtriomlem  10425  axdc2lem  10431  axcclem  10440  brdom7disj  10514  brdom6disj  10515  iundom2g  10523  konigthlem  10552  canthwelem  10634  wunex2  10722  wunex3  10725  1nq  10912  1pr  10999  nrex1  11048  axcnex  11131  ax1cn  11133  pnfex  11261  mnfxr  11265  cju  12213  nnexALT  12234  2nn  12313  2re  12314  2cn  12315  3nn  12319  3re  12320  3cn  12321  4nn  12323  4re  12324  4cn  12325  5nn  12326  5re  12327  5cn  12328  6nn  12329  6re  12330  6cn  12331  7nn  12332  7re  12333  7cn  12334  8nn  12335  8re  12336  8cn  12337  9nn  12338  9re  12339  9cn  12340  nn0ex  12509  zexALT  12610  nneo  12679  zeo  12681  deccl  12725  10re  12733  decnncl  12734  numnncl2  12738  decnncl2  12739  numsucc  12755  numma2c  12761  numadd  12762  numaddc  12763  nummul1c  12764  nummul2c  12765  decmul1  12779  qexALT  12987  xrex  13010  xnegex  13233  xnegcl  13238  ixxssxr  13383  fz0to4untppr  13657  fz0to5un2tp  13658  om2uzuzi  13984  ltweuz  13996  axdc4uzlem  14018  seqex  14038  seqexw  14052  m1expcl2  14120  faccl  14318  facwordi  14324  faclbnd2  14326  bccl  14357  hashen1  14405  hashrabrsn  14407  hashunlei  14461  hashpw  14472  tpf1o  14537  s1cli  14642  ccat2s1p1  14666  cats1un  14757  revs1  14801  cshwsexa  14860  cats1cli  14893  cats1fvn  14894  crre  15164  remim  15167  climmpt  15621  sumex  15738  supcvg  15909  geo2lim  15928  prodex  15958  bpoly4  16112  ere  16142  eftlub  16164  efsep  16165  tan0  16206  ef01bndlem  16239  nn0o  16440  divalglem5  16454  divalglem9  16458  sadcf  16510  smupf  16535  crth  16836  phimullem  16837  pczpre  16906  pockthi  16966  prmreclem2  16976  igz  16993  0ramcl  17082  1259lem1  17190  1259lem2  17191  1259lem3  17192  1259lem4  17193  1259lem5  17194  1259prm  17195  2503lem1  17196  2503lem2  17197  2503lem3  17198  2503prm  17199  4001lem1  17200  4001lem2  17201  4001lem3  17202  4001lem4  17203  4001prm  17204  strle1  17217  ndxarg  17255  basendxnn  17278  plusgndxnn  17337  tsetndxnn  17406  plendxnn  17420  dsndxnn  17439  unifndxnn  17449  prdsbasex  17502  prdsds  17516  yonedalem3  18335  isposix  18379  chnub  18677  plusffval  18703  issubmgm2  18760  efmnd1hash  18950  efmnd2hash  18952  smndex1bas  18967  smndex1sgrp  18969  smndex1mnd  18971  smndex1id  18972  smndex2dbas  18975  smndex2hbas  18977  grpsubfval  19049  mulgfval  19134  symg1hash  19459  symg2hash  19461  symgvalstruct  19466  symgfisg  19537  psgnsn  19589  psgnprfval1  19591  odfval  19601  sylow2alem2  19687  efgsval2  19802  efgsp1  19806  pgpfaclem1  20152  dvdsrval  20442  isirred  20500  scaffval  20978  prmidl0  21446  cnfldex  21493  xrsex  21507  pzriprnglem4  21602  pzriprnglem5  21603  pzriprnglem6  21604  pzriprng1ALT  21614  znle  21654  znidomb  21679  cnmsgnsubg  21695  refld  21737  ipffval  21766  psrbag0  22181  psrbagsn  22182  psr1baslem  22313  mat1dimbas  22597  mat1dimscm  22600  mat1f1o  22603  mat1rhmelval  22605  m2detleib  22756  pmatcoe1fsupp  22826  indistopon  23126  iccordt  23339  conncompid  23556  ptbasfi  23706  ptcmpfi  23938  ustfn  24327  ust0  24345  ustn0  24346  tmslem  24607  nmfval  24713  cnbl0  24898  cnopn  24911  remet  24915  re2ndc  24926  zcld  24939  icccmp  24951  xrge0gsumle  24959  xrge0tsms  24960  xmetdcn  24964  divcn  24995  expcn  24999  iiconn  25014  idcncf  25045  cnmpopc  25055  cnrehmeo  25080  cnheiborlem  25081  rellycmp  25084  bndth  25085  evth2  25087  cnrlmod  25270  cnrlvec  25271  cncmet  25449  ishl2  25497  ehleudis  25545  ehleudisval  25546  finiunmbl  25671  ioombl1lem4  25688  vitalilem4  25738  vitalilem5  25739  ismbf2d  25767  mbfimaopnlem  25782  mbfi1fseqlem6  25847  itgex  25897  bddmulibl  25966  ditgex  25979  recnperf  26032  dvcnvrelem2  26145  ftc1  26169  mdegcl  26194  plyeq0lem  26335  aaliou3lem4  26475  dvradcnv  26549  sincn  26572  coscn  26573  tanabsge  26636  circsubm  26683  reloggim  26729  logcn  26777  dvloglem  26778  logdmopn  26779  dvlog2  26783  2irrexpq  26861  cxpcn  26875  cxpcn3  26878  resqrtcn  26879  2logb9irrALT  26928  2irrexpqALT  26930  atanrecl  27041  atan1  27058  atansopn  27062  birthdaylem1  27081  birthday  27084  emcllem4  27128  emcllem6  27130  lgamgulmlem6  27163  basellem6  27215  ppiublem1  27331  bposlem6  27418  bposlem8  27420  lgslem4  27429  lgsdir2lem2  27455  selberglem1  27674  selberglem3  27676  selberg  27677  selbergs  27703  qdrng  27749  0no  27967  1no  27968  lrrecse  28100  precsexlem11  28375  seqsex  28443  nnsex  28476  n0bday  28510  n0subs  28521  n0p1nns  28529  dfnns2  28530  zsex  28538  bdayfinbndlem1  28625  z12sex  28632  z12shalf  28638  edgfndxnn  29282  structvtxvallem  29310  usgrexmpllem  29550  usgrexmpl  29553  uhgrspan1  29593  upgrres  29596  umgrres  29597  usgrres  29598  upgrres1  29603  umgrres1  29604  usgrres1  29605  fusgrfis  29620  cusgrres  29738  vtxdlfgrval  29775  vtxdusgr0edgnelALT  29786  umgr2v2e  29815  vtxdginducedm1lem1  29829  vtxdginducedm1fi  29834  finsumvtxdg2ssteplem4  29838  pthdlem1  30055  crctcshlem3  30108  2wlkd  30225  2wlkond  30226  2trlond  30228  2pthd  30229  2pthond  30231  umgr2adedgwlkonALT  30236  0pth  30416  wlk2v2e  30448  3wlkd  30461  3trlond  30464  3pthd  30465  3pthond  30466  3spthond  30468  eupthvdres  30526  eulerpathpr  30531  konigsbergumgr  30542  konigsberglem5  30547  konigsberg  30548  ex-lcm  30749  isvciOLD  30872  isnvi  30905  blocni  31097  hmoval  31102  cncph  31111  ipasslem7  31128  siilem2  31144  normlem2  31403  normlem3  31404  normlem6  31407  h0elch  31547  hhssabloilem  31553  hhsssh  31561  spansnji  31938  nonbooli  31943  3oalem5  31958  3oalem6  31959  3oai  31960  mayetes3i  32021  nmcexi  32318  nmbdfnlb  32342  rnelshi  32351  cnlnadjlem5  32363  pjbdlni  32441  golem2  32564  goeqi  32565  dp2clq  33140  rpdp2cl  33141  rpdp2cl2  33142  dpmul100  33156  rpdpcl  33162  xrge0tsmsd  33333  pmtrto1cl  33359  psgnfzto1stlem  33360  fzto1st  33363  psgnfzto1st  33365  nn0omnd  33606  xrge0slmod  33610  qusima  33660  fply1  33792  extvfvcl  33870  ply1degltdimlem  33956  ccfldextdgrr  34006  algextdeglem8  34058  constrfin  34080  2sqr3minply  34114  2sqr3nconstr  34115  cos9thpiminplylem4  34119  cos9thpiminplylem5  34120  cos9thpinconstrlem2  34124  circtopn  34171  circcn  34172  zarcmplem  34215  tpr2tp  34238  tpr2rico  34246  ordtprsval  34252  ordtprsuni  34253  ordtrestNEW  34255  ordtrest2NEWlem  34256  ordtrest2NEW  34257  ordtconnlem1  34258  mndpluscn  34260  xrge0pluscn  34274  xrge0mulc1cn  34275  xrge0haus  34278  lmlimxrge0  34282  lmxrge0  34286  qqhcn  34325  qqhucn  34326  esumex  34363  esumcst  34397  hasheuni  34419  esumcvg  34420  prsiga  34465  brsiga  34517  mbfmcnt  34602  sxbrsigalem3  34606  dya2iocuni  34617  dya2iocucvr  34618  sxbrsigalem1  34619  sxbrsiga  34624  eulerpartlemt  34705  fibp1  34735  coinflipprob  34814  coinfliprv  34817  ccatmulgnn0dir  34876  signswplusg  34886  hgt750lem2  34983  hgt750leme  34989  bnj105  35057  bnj918  35099  bnj95  35196  bnj852  35253  bnj865  35255  fineqvnttrclse  35459  subfacp1lem1  35569  subfacp1lem3  35572  subfacp1lem5  35574  subfacp1lem6  35575  kur14lem7  35602  iisconn  35642  iillysconn  35643  cvmliftlem5  35679  cvmliftlem8  35682  cvmliftlem10  35684  cvmlift2lem9  35701  satfv0  35748  goalrlem  35786  goalr  35787  satffunlem2lem2  35796  circum  36064  iexpire  36125  altopex  36350  colinearex  36450  ssoninhaus  36847  cnndvlem2  37015  bj-prex  37563  bj-prfromadj  37568  bj-pinftyccb  37752  taupi  37854  isbasisrelowl  37891  relowlpssretop  37897  poimirlem29  38187  poimirlem30  38188  poimirlem31  38189  dvasin  38242  dvacos  38243  areacirc  38251  upixp  38267  fdc  38283  lmclim2  38296  cncfres  38303  heibor1lem  38347  rrnval  38365  rrnmet  38367  reheibor  38377  isdrngo2  38496  isrngohom  38503  idlval  38551  isidl  38552  igenval  38599  scottexf  38706  cnvepresex  38874  preex  39030  renegclALT  39626  ldualfvadd  39791  cmtfvalN  39873  cvrfval  39931  cdleme31fv  41053  cdlemk40  41580  cdlemk56  41634  dibopelvalN  41806  dibopelval2  41808  dibelval3  41810  diblsmopel  41834  cdlemn11a  41870  dihopelvalcpre  41911  dihpN  41999  hlhilsca  42598  hlhilip  42611  3factsumint1  42677  lcmineqlem23  42707  aks4d1p1p6  42729  aks4d1p1p5  42731  aks6d1c6isolem2  42831  25or6to4  42862  itrere  42968  acos1half  43008  redvmptabs  43010  readvrec2  43011  sn-0tie0  43114  sn-itrere  43151  sn-retire  43152  prjspval  43226  flt4lem5e  43279  sn-isghm  43296  mapfzcons2  43341  jm2.23  43614  jm2.27dlem2  43628  jm2.27dlem4  43630  rmydioph  43632  rmxdioph  43634  expdiophlem2  43640  expdioph  43641  aomclem6  43677  pwslnmlem0  43709  frlmpwfi  43716  mncn0  43757  aaitgo  43780  arearect  43833  areaquad  43834  omcl3g  43952  comptiunov2i  44323  frege110  44590  frege133  44613  radcnvrat  44915  uzmptshftfval  44947  dvradcnv2  44948  binomcxplemdvbinom  44954  binomcxplemcvg  44955  binomcxplemnotnn0  44957  permaxinf2lem  45612  rfcnpre1  45630  fcnre  45636  refsumcn  45641  refsum2cnlem1  45648  unirnmapsn  45821  infxrpnf  46051  iocopn  46127  icoopn  46132  mccl  46205  clim1fr1  46208  islptre  46226  sumnnodd  46237  lptre2pt  46245  limclner  46256  limclr  46260  expfac  46262  0cnf  46482  icccncfext  46492  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  itgsin0pilem1  46555  iblempty  46570  itgvol0  46573  stoweidlem47  46652  stoweidlem53  46658  stoweidlem57  46662  stoweidlem59  46664  wallispilem3  46672  wallispilem4  46673  wallispilem5  46674  wallispi  46675  stirlinglem1  46679  stirlinglem8  46686  stirlinglem12  46690  stirlinglem13  46691  stirlinglem14  46692  stirlinglem15  46693  dirkerper  46701  dirkercncflem2  46709  fourierdlem16  46728  fourierdlem21  46733  fourierdlem22  46734  fourierdlem36  46748  fourierdlem42  46754  fourierdlem71  46782  fourierdlem83  46794  fourierdlem102  46813  fourierdlem103  46814  fourierdlem104  46815  fourierdlem111  46822  fourierdlem112  46823  fourierdlem114  46825  sqwvfoura  46833  sqwvfourb  46834  fourierswlem  46835  fouriersw  46836  etransclem48  46887  salexct3  46947  salgencntex  46948  salgensscntex  46949  iooborel  46956  bor1sal  46960  gsumge0cl  46976  sge0tsms  46985  sge0isum  47032  nnfoctbdjlem  47060  isomenndlem  47135  mbfresmf  47344  incsmflem  47346  incsmf  47347  smfmbfcex  47365  decsmflem  47371  decsmf  47372  smflimlem1  47376  smfpimbor1lem2  47404  smf2id  47406  smfco  47407  smfpimcclem  47412  goldrarr  47506  lambert0  47512  sprsymrelfolem1  48129  sprbisymrel  48136  fmtno0prm  48198  fmtno1prm  48199  fmtno2prm  48200  fmtno3prm  48202  fmtno4prm  48215  m2prm  48231  m3prm  48232  m5prm  48238  m7prm  48240  lighneallem4a  48248  nprmdvdsfacm1lem4  48263  0evenALTV  48341  1oddALTV  48343  2evenALTV  48345  6even  48364  7odd  48365  8even  48366  9gbo  48427  opstrgric  48579  ushggricedg  48580  grtri  48593  usgrexmpl1  48675  usgrexmpl1vtx  48676  usgrexmpl1edg  48677  usgrexmpl2  48680  usgrexmpl2vtx  48681  usgrexmpl2edg  48682  gpgprismgr4cycllem5  48752  pgnbgreunbgr  48778  pgn4cyclex  48779  uspgrex  48803  lmod1zrnlvec  49158  zlmodzxzldeplem1  49164  zlmodzxzldeplem3  49166  zlmodzxzldeplem4  49167  zlmodzxzldep  49168  ldepsnlinclem1  49169  ldepsnlinclem2  49170  blennn0elnn  49241  nn0sumshdiglemA  49283  nn0sumshdiglemB  49284  itcovalpclem2  49335  itcovalt2lem2  49340  ackval42  49360  rrx2line  49404  rrx2linesl  49407  spheres  49410  2sphere  49413  2sphere0  49414  line2x  49418  line2y  49419  resipos  49637  functhinclem1  50106  prsthinc  50126  setc1oterm  50153  funcsetc1ocl  50158  funcsetc1o  50159  isinito2lem  50160  isinito3  50162  functermc2  50171  incat  50263  setc1onsubc  50264