Theorem eqeltri 2857

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836

This theorem is used by:  eqeltrri  2858  3eltr4i  2874  intab  4938  axrep6g  5243  unisn2  5266  inex2  5278  vpwex  5339  ord3ex  5349  zfpair  5383  vsnex  5393  snex  5397  opex  5432  opexOLD  5433  otex  5434  uniopel  5489  elvvuni  5728  isarep2  6627  fvex  6896  fvexi  6897  riotaex  7379  ovexi  7452  tpex  7760  oprabex  7986  oprabrexex2  7988  mpoexw  8089  mptmpoopabbrd  8092  tfrlem16  8394  1oex  8479  2oex  8481  1on  8482  2on  8483  3on  8486  4on  8487  oesuclem  8526  oecl  8538  o2p2e4  8542  nnecl  8615  1onnALT  8643  2onnALT  8645  3onn  8646  4onn  8647  mapsnf1o2  8915  sbthlem10  9108  cnvfi  9184  fnfi  9186  nnunifi  9276  pwfi  9303  prfiALT  9309  tpfi  9310  fczfsuppd  9371  cantnfvalf  9659  oemapwe  9688  cantnffval2  9689  cnfcom3clem  9699  ssttrcl  9709  r1fin  9773  scottex  9926  scottex2OLD  9939  hta  9955  htaOLD  9956  infxpenlem  10085  alephon  10141  alephfplem1  10176  dfac5lem4  10198  dfac5lem5  10199  kmlem10  10231  fin1a2lem10  10480  fin1a2lem12  10482  hsmexlem9  10496  axcc2lem  10507  domtriomlem  10513  axdc2lem  10519  axcclem  10528  brdom7disj  10603  brdom6disj  10604  iundom2g  10617  konigthlem  10646  canthwelem  10728  wunex2  10816  wunex3  10819  hftsk  10857  1nq  11006  1pr  11093  nrex1  11142  axcnex  11225  ax1cn  11227  pnfex  11355  mnfxr  11359  cju  12309  nnexALT  12330  2nn  12409  2re  12410  2cn  12411  3nn  12415  3re  12416  3cn  12417  4nn  12419  4re  12420  4cn  12421  5nn  12422  5re  12423  5cn  12424  6nn  12425  6re  12426  6cn  12427  7nn  12428  7re  12429  7cn  12430  8nn  12431  8re  12432  8cn  12433  9nn  12434  9re  12435  9cn  12436  nn0ex  12605  zexALT  12706  nneo  12776  zeo  12778  deccl  12822  10re  12830  decnncl  12831  numnncl2  12835  decnncl2  12836  numsucc  12852  numma2c  12858  numadd  12859  numaddc  12860  nummul1c  12861  nummul2c  12862  decmul1  12876  qexALT  13084  xrex  13108  xnegex  13331  xnegcl  13336  ixxssxr  13481  fz0to4untppr  13757  fz0to5un2tp  13758  om2uzuzi  14085  ltweuz  14097  axdc4uzlem  14119  seqex  14139  seqexw  14153  m1expcl2  14221  faccl  14420  facwordi  14426  faclbnd2  14428  bccl  14459  hashen1  14507  hashrabrsn  14509  hashunlei  14563  hashpw  14574  tpf1o  14639  s1cli  14745  ccat2s1p1  14770  cats1un  14863  revs1  14907  cshwsexa  14968  cats1cli  15001  cats1fvn  15002  crre  15274  remim  15277  climmpt  15731  sumex  15848  supcvg  16018  geo2lim  16037  prodex  16067  bpoly4  16218  ere  16248  eftlub  16270  efsep  16271  tan0  16312  ef01bndlem  16345  nn0o  16546  divalglem5  16560  divalglem9  16564  sadcf  16616  smupf  16641  crth  16948  phimullem  16949  pczpre  17018  pockthi  17078  prmreclem2  17088  igz  17105  0ramcl  17194  1259lem1  17302  1259lem2  17303  1259lem3  17304  1259lem4  17305  1259lem5  17306  1259prm  17307  2503lem1  17308  2503lem2  17309  2503lem3  17310  2503prm  17311  4001lem1  17312  4001lem2  17313  4001lem3  17314  4001lem4  17315  4001prm  17316  strle1  17329  ndxarg  17367  basendxnn  17390  plusgndxnn  17449  tsetndxnn  17518  plendxnn  17532  dsndxnn  17551  unifndxnn  17561  prdsbasex  17614  prdsds  17628  yonedalem3  18447  isposix  18491  chnub  18789  plusffval  18815  issubmgm2  18885  efmnd1hash  19081  efmnd2hash  19083  smndex1bas  19098  smndex1sgrp  19100  smndex1mnd  19102  smndex1id  19103  smndex2dbas  19106  smndex2hbas  19108  grpsubfval  19187  mulgfval  19272  symg1hash  19597  symg2hash  19599  symgvalstruct  19604  symgfisg  19675  psgnsn  19727  psgnprfval1  19729  odfval  19739  sylow2alem2  19825  efgsval2  19940  efgsp1  19944  pgpfaclem1  20290  dvdsrval  20584  isirred  20642  scaffval  21148  prmidl0  21627  cnfldex  21674  xrsex  21688  pzriprnglem4  21783  pzriprnglem5  21784  pzriprnglem6  21785  pzriprng1ALT  21795  znle  21835  znidomb  21860  cnmsgnsubg  21876  refld  21918  ipffval  21947  psrbag0  22364  psrbagsn  22365  psr1baslem  22496  mat1dimbas  22780  mat1dimscm  22783  mat1f1o  22786  mat1rhmelval  22788  m2detleib  22939  pmatcoe1fsupp  23012  indistopon  23312  iccordt  23525  conncompid  23742  ptbasfi  23893  ptcmpfi  24125  ustfn  24514  ust0  24532  ustn0  24533  tmslem  24794  nmfval  24900  cnbl0  25085  cnopn  25098  remet  25102  re2ndc  25113  zcld  25126  icccmp  25138  xrge0gsumle  25146  xrge0tsms  25147  xmetdcn  25151  divcn  25182  expcn  25186  iiconn  25201  idcncf  25232  cnmpopc  25242  cnrehmeo  25267  cnheiborlem  25268  rellycmp  25271  bndth  25272  evth2  25274  cnrlmod  25457  cnrlvec  25458  cncmet  25636  ishl2  25684  ehleudis  25732  ehleudisval  25733  finiunmbl  25858  ioombl1lem4  25875  vitalilem4  25925  vitalilem5  25926  ismbf2d  25954  mbfimaopnlem  25969  mbfi1fseqlem6  26034  itgex  26084  bddmulibl  26152  ditgex  26165  recnperf  26218  dvcnvrelem2  26331  ftc1  26355  mdegcl  26380  plyeq0lem  26522  iaa  26644  aaliou3lem4  26666  dvradcnv  26741  sincn  26764  coscn  26765  tanabsge  26828  circsubm  26874  reloggim  26920  logcn  26968  dvloglem  26969  logdmopn  26970  dvlog2  26974  2irrexpq  27052  cxpcn  27066  cxpcn3  27069  resqrtcn  27070  2logb9irrALT  27119  2irrexpqALT  27121  atanrecl  27232  atan1  27249  atansopn  27253  birthdaylem1  27272  birthday  27275  emcllem4  27319  emcllem6  27321  lgamgulmlem6  27354  basellem6  27406  ppiublem1  27522  bposlem6  27609  bposlem8  27611  lgslem4  27620  lgsdir2lem2  27646  selberglem1  27865  selberglem3  27867  selberg  27868  selbergs  27894  qdrng  27940  flt4lem5e  27979  0no  28188  1no  28189  lrrecse  28321  precsexlem11  28596  seqsex  28664  nnsex  28697  n0bday  28731  n0subs  28742  n0p1nns  28750  dfnns2  28751  zsex  28759  bdayfinbndlem1  28846  z12sex  28853  z12shalf  28859  angmgmlem  29388  edgfndxnn  29563  structvtxvallem  29591  usgrexmpllem  29834  usgrexmpl  29837  uhgrspan1  29877  upgrres  29880  umgrres  29881  usgrres  29882  upgrres1  29887  umgrres1  29888  usgrres1  29889  fusgrfis  29904  cusgrres  30022  vtxdlfgrval  30059  vtxdusgr0edgnelALT  30070  umgr2v2e  30099  vtxdginducedm1lem1  30113  vtxdginducedm1fi  30118  finsumvtxdg2ssteplem4  30122  pthdlem1  30345  crctcshlem3  30401  2wlkd  30518  2wlkond  30519  2trlond  30521  2pthd  30522  2pthond  30524  umgr2adedgwlkonALT  30529  0pth  30709  wlk2v2e  30751  3wlkd  30764  3trlond  30767  3pthd  30768  3pthond  30769  3spthond  30771  eupthvdres  30829  eulerpathpr  30834  konigsbergumgr  30845  konigsberglem5  30850  konigsberg  30851  ex-lcm  31052  isvciOLD  31175  isnvi  31208  blocni  31400  hmoval  31405  cncph  31414  ipasslem7  31431  siilem2  31447  normlem2  31706  normlem3  31707  normlem6  31710  h0elch  31850  hhssabloilem  31856  hhsssh  31864  spansnji  32241  nonbooli  32246  3oalem5  32261  3oalem6  32262  3oai  32263  mayetes3i  32324  nmcexi  32621  nmbdfnlb  32645  rnelshi  32654  cnlnadjlem5  32666  pjbdlni  32744  golem2  32867  goeqi  32868  dp2clq  33440  rpdp2cl  33441  rpdp2cl2  33442  dpmul100  33456  rpdpcl  33462  xrge0tsmsd  33627  pmtrto1cl  33653  psgnfzto1stlem  33654  fzto1st  33657  psgnfzto1st  33659  nn0omnd  33898  xrge0slmod  33902  qusima  33952  fply1  34083  extvfvcl  34161  ply1degltdimlem  34247  ccfldextdgrr  34297  algextdeglem8  34349  constrfin  34371  2sqr3minply  34405  2sqr3nconstr  34406  cos9thpiminplylem4  34410  cos9thpiminplylem5  34411  cos9thpinconstrlem2  34415  circtopn  34462  circcn  34463  zarcmplem  34506  tpr2tp  34529  tpr2rico  34537  ordtprsval  34543  ordtprsuni  34544  ordtrestNEW  34546  ordtrest2NEWlem  34547  ordtrest2NEW  34548  ordtconnlem1  34549  mndpluscn  34551  xrge0pluscn  34565  xrge0mulc1cn  34566  xrge0haus  34569  lmlimxrge0  34573  lmxrge0  34577  qqhcn  34616  qqhucn  34617  esumex  34654  esumcst  34688  hasheuni  34710  esumcvg  34711  prsiga  34756  brsiga  34809  mbfmcnt  34893  sxbrsigalem3  34897  dya2iocuni  34908  dya2iocucvr  34909  sxbrsigalem1  34910  sxbrsiga  34915  eulerpartlemt  34996  fibp1  35026  coinflipprob  35105  coinfliprv  35108  ccatmulgnn0dir  35167  signswplusg  35177  hgt750lem2  35274  hgt750leme  35280  bnj105  35348  bnj918  35390  bnj95  35487  bnj852  35544  bnj865  35546  5on  35754  6on  35755  7on  35756  8on  35757  9on  35758  5onn  35759  6onn  35760  7onn  35761  8onn  35762  9onn  35763  fineqvnttrclse  35775  subfacp1lem1  35923  subfacp1lem3  35926  subfacp1lem5  35928  subfacp1lem6  35929  kur14lem7  35956  iisconn  35996  iillysconn  35997  cvmliftlem5  36033  cvmliftlem8  36036  cvmliftlem10  36038  cvmlift2lem9  36055  satfv0  36102  goalrlem  36140  goalr  36141  satffunlem2lem2  36150  circum  36418  iexpire  36479  altopex  36705  colinearex  36805  ssoninhaus  37216  cnndvlem2  37384  bj-prex  37933  bj-prfromadj  37938  bj-pinftyccb  38122  taupi  38224  isbasisrelowl  38261  relowlpssretop  38267  poimirlem29  38547  poimirlem30  38548  poimirlem31  38549  dvasin  38602  dvacos  38603  areacirc  38611  upixp  38643  fdc  38659  lmclim2  38672  cncfres  38679  heibor1lem  38723  rrnval  38741  rrnmet  38743  reheibor  38753  isdrngo2  38872  isrngohom  38879  idlval  38927  isidl  38928  igenval  38975  scottexf  39080  cnvepresex  39248  preex  39404  renegclALT  40000  ldualfvadd  40165  cmtfvalN  40247  cvrfval  40305  cdleme31fv  41427  cdlemk40  41954  cdlemk56  42008  dibopelvalN  42180  dibopelval2  42182  dibelval3  42184  diblsmopel  42208  cdlemn11a  42244  dihopelvalcpre  42285  dihpN  42373  hlhilsca  42972  hlhilip  42985  3factsumint1  43051  lcmineqlem23  43081  aks4d1p1p6  43103  aks4d1p1p5  43105  aks6d1c6isolem2  43205  25or6to4  43236  itrere  43355  acos1half  43389  redvmptabs  43391  readvrec2  43392  sn-0tie0  43495  sn-itrere  43532  sn-retire  43533  prjspval  43611  sn-isghm  43664  mapfzcons2  43709  jm2.23  43982  jm2.27dlem2  43996  jm2.27dlem4  43998  rmydioph  44000  rmxdioph  44002  expdiophlem2  44008  expdioph  44009  aomclem6  44045  pwslnmlem0  44077  frlmpwfi  44084  mncn0  44125  aaitgo  44148  arearect  44201  areaquad  44202  omcl3g  44320  comptiunov2i  44691  frege110  44958  frege133  44981  radcnvrat  45283  uzmptshftfval  45315  dvradcnv2  45316  binomcxplemdvbinom  45322  binomcxplemcvg  45323  binomcxplemnotnn0  45325  permaxinf2lem  45980  rfcnpre1  46005  fcnre  46011  refsumcn  46016  refsum2cnlem1  46023  unirnmapsn  46196  infxrpnf  46425  iocopn  46501  icoopn  46506  mccl  46579  clim1fr1  46582  islptre  46600  sumnnodd  46611  lptre2pt  46619  limclner  46630  limclr  46634  expfac  46636  0cnf  46856  icccncfext  46866  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  itgsin0pilem1  46929  iblempty  46944  itgvol0  46947  stoweidlem47  47026  stoweidlem53  47032  stoweidlem57  47036  stoweidlem59  47038  wallispilem3  47046  wallispilem4  47047  wallispilem5  47048  wallispi  47049  stirlinglem1  47053  stirlinglem8  47060  stirlinglem12  47064  stirlinglem13  47065  stirlinglem14  47066  stirlinglem15  47067  dirkerper  47075  dirkercncflem2  47083  fourierdlem16  47102  fourierdlem21  47107  fourierdlem22  47108  fourierdlem36  47122  fourierdlem42  47128  fourierdlem71  47156  fourierdlem83  47168  fourierdlem102  47187  fourierdlem103  47188  fourierdlem104  47189  fourierdlem111  47196  fourierdlem112  47197  fourierdlem114  47199  sqwvfoura  47207  sqwvfourb  47208  fourierswlem  47209  fouriersw  47210  etransclem48  47261  salexct3  47321  salgencntex  47322  salgensscntex  47323  iooborel  47330  bor1sal  47334  gsumge0cl  47350  sge0tsms  47359  sge0isum  47406  nnfoctbdjlem  47434  isomenndlem  47509  mbfresmf  47718  incsmflem  47720  incsmf  47721  smfmbfcex  47739  decsmflem  47745  decsmf  47746  smflimlem1  47750  smfpimbor1lem2  47778  smf2id  47780  smfco  47781  smfpimcclem  47786  goldrarr  47897  lambert0  47906  tannpoly  47909  sprsymrelfolem1  48543  sprbisymrel  48550  fmtno0prm  48612  fmtno1prm  48613  fmtno2prm  48614  fmtno3prm  48616  fmtno4prm  48629  m2prm  48645  m3prm  48646  m5prm  48652  m7prm  48654  lighneallem4a  48662  nprmdvdsfacm1lem4  48677  0evenALTV  48755  1oddALTV  48757  2evenALTV  48759  6even  48778  7odd  48779  8even  48780  9gbo  48841  opstrgric  48993  ushggricedg  48994  grtri  49007  usgrexmpl1  49089  usgrexmpl1vtx  49090  usgrexmpl1edg  49091  usgrexmpl2  49094  usgrexmpl2vtx  49095  usgrexmpl2edg  49096  gpgprismgr4cycllem5  49166  pgnbgreunbgr  49192  pgn4cyclex  49193  uspgrex  49217  lmod1zrnlvec  49575  zlmodzxzldeplem1  49581  zlmodzxzldeplem3  49583  zlmodzxzldeplem4  49584  zlmodzxzldep  49585  ldepsnlinclem1  49586  ldepsnlinclem2  49587  blennn0elnn  49658  nn0sumshdiglemA  49700  nn0sumshdiglemB  49701  itcovalpclem2  49752  itcovalt2lem2  49757  ackval42  49777  rrx2line  49821  rrx2linesl  49824  spheres  49827  2sphere  49830  2sphere0  49831  line2x  49835  line2y  49836  resipos  50052  functhinclem1  50521  prsthinc  50541  setc1oterm  50568  funcsetc1ocl  50573  funcsetc1o  50574  isinito2lem  50575  isinito3  50577  functermc2  50586  incat  50678  setc1onsubc  50679