Theorem eqeltri 2827

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

Syntax hints:   = wceq 1543   ∈ wcel 2112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-clel 2809

This theorem is referenced by:  eqeltrri  2828  3eltr4i  2844  intab  4875  unisn2  5190  inex2  5196  vpwex  5255  ord3ex  5265  zfpair  5299  opex  5333  otex  5334  uniopel  5384  elvvuni  5610  predasetex  6155  isarep2  6447  fvex  6708  fvexi  6709  riotaex  7152  ovexi  7225  tpex  7510  oprabex  7727  oprabrexex2  7729  mpoexw  7827  tfrlem16  8107  1on  8187  2on  8188  3on  8190  4on  8191  1oex  8193  2oex  8197  2oexOLD  8198  oesuclem  8230  oecl  8242  o2p2e4  8246  nnecl  8319  1onn  8345  2onn  8346  3onn  8347  4onn  8348  mapsnf1o2  8553  sbthlem10  8743  imafi  8830  pwfi  8833  cnvfi  8834  fnfi  8835  nnunifi  8900  xpfi  8920  prfi  8924  tpfi  8925  pwfiOLD  8949  fczfsuppd  8981  cantnfvalf  9258  oemapwe  9287  cantnffval2  9288  cnfcom3clem  9298  trpredex  9321  r1fin  9354  hta  9478  infxpenlem  9592  alephon  9648  alephfplem1  9683  dfac5lem4  9705  dfac5lem5  9706  kmlem10  9738  fin1a2lem10  9988  fin1a2lem12  9990  hsmexlem9  10004  axcc2lem  10015  domtriomlem  10021  axdc2lem  10027  axcclem  10036  brdom7disj  10110  brdom6disj  10111  iundom2g  10119  konigthlem  10147  canthwelem  10229  wunex2  10317  wunex3  10320  1nq  10507  1pr  10594  nrex1  10643  axcnex  10726  ax1cn  10728  pnfex  10851  mnfxr  10855  inelr  11785  cju  11791  nnexALT  11797  2nn  11868  2re  11869  2cn  11870  3nn  11874  3re  11875  3cn  11876  4nn  11878  4re  11879  4cn  11880  5nn  11881  5re  11882  5cn  11883  6nn  11884  6re  11885  6cn  11886  7nn  11887  7re  11888  7cn  11889  8nn  11890  8re  11891  8cn  11892  9nn  11893  9re  11894  9cn  11895  nn0ex  12061  zexALT  12161  nneo  12226  zeo  12228  deccl  12273  10re  12277  decnncl  12278  numnncl2  12281  decnncl2  12282  numsucc  12298  numma2c  12304  numadd  12305  numaddc  12306  nummul1c  12307  nummul2c  12308  decmul1  12322  qexALT  12525  xrex  12548  xnegex  12763  xnegcl  12768  ixxssxr  12912  om2uzuzi  13487  ltweuz  13499  axdc4uzlem  13521  seqex  13541  seqexw  13555  m1expcl2  13622  faccl  13814  facwordi  13820  faclbnd2  13822  bccl  13853  hashen1  13902  hashrabrsn  13904  hashunlei  13957  hashpw  13968  s1cli  14127  ccat2s1p1  14153  cats1un  14251  revs1  14295  cshwsexa  14354  cats1cli  14387  cats1fvn  14388  crre  14642  remim  14645  climmpt  15097  sumex  15216  supcvg  15383  geo2lim  15402  prodex  15432  bpoly4  15584  ere  15613  eftlub  15633  efsep  15634  tan0  15675  ef01bndlem  15708  nn0o  15907  divalglem5  15921  divalglem9  15925  sadcf  15975  smupf  16000  crth  16294  phimullem  16295  pczpre  16363  pockthi  16423  prmreclem2  16433  igz  16450  0ramcl  16539  1259lem1  16647  1259lem2  16648  1259lem3  16649  1259lem4  16650  1259lem5  16651  1259prm  16652  2503lem1  16653  2503lem2  16654  2503lem3  16655  2503prm  16656  4001lem1  16657  4001lem2  16658  4001lem3  16659  4001lem4  16660  4001prm  16661  ndxarg  16690  basendxnn  16731  basendxnnOLD  16732  strle1  16776  prdsbasex  16909  prdsds  16923  yonedalem3  17742  isposix  17786  plusffval  18074  efmnd1hash  18273  efmnd2hash  18275  smndex1bas  18287  smndex1sgrp  18289  smndex1mnd  18291  smndex1id  18292  smndex2dbas  18295  smndex2hbas  18297  grpsubfval  18365  mulgfval  18444  symg1hash  18736  symg2hash  18738  symgvalstruct  18743  symgfisg  18814  psgnsn  18866  psgnprfval1  18868  odfval  18878  sylow2alem2  18961  efgsval2  19077  efgsp1  19081  pgpfaclem1  19422  dvdsrval  19617  isirred  19671  scaffval  19871  xrsex  20332  zlmlem  20437  znle  20455  znidomb  20480  cnmsgnsubg  20493  refld  20535  ipffval  20564  psrbag0  20974  psrbagsn  20975  psr1baslem  21060  mat1dimbas  21323  mat1dimscm  21326  mat1f1o  21329  mat1rhmelval  21331  m2detleib  21482  pmatcoe1fsupp  21552  indistopon  21852  iccordt  22065  conncompid  22282  ptbasfi  22432  ptcmpfi  22664  ustfn  23053  ust0  23071  ustn0  23072  tmslem  23334  nmfval  23440  tnglem  23492  cnbl0  23625  cnopn  23638  remet  23641  re2ndc  23652  zcld  23664  icccmp  23676  xrge0gsumle  23684  xrge0tsms  23685  xmetdcn  23689  divcn  23719  expcn  23723  iiconn  23738  idcncf  23769  cnmpopc  23779  cnrehmeo  23804  cnheiborlem  23805  rellycmp  23808  bndth  23809  evth2  23811  cnrlmod  23994  cnrlvec  23995  cncmet  24173  ishl2  24221  ehleudis  24269  ehleudisval  24270  finiunmbl  24395  ioombl1lem4  24412  vitalilem4  24462  vitalilem5  24463  ismbf2d  24491  mbfimaopnlem  24506  mbfi1fseqlem6  24572  itgex  24622  bddmulibl  24690  ditgex  24703  recnperf  24756  dvcnvrelem2  24869  ftc1  24893  mdegcl  24921  plyeq0lem  25058  aaliou3lem4  25193  dvradcnv  25267  sincn  25290  coscn  25291  tanabsge  25350  circsubm  25396  reloggim  25441  logcn  25489  dvloglem  25490  logdmopn  25491  dvlog2  25495  2irrexpq  25572  cxpcn  25585  cxpcn3  25588  resqrtcn  25589  2logb9irrALT  25635  2irrexpqALT  25637  atanrecl  25748  atan1  25765  atansopn  25769  birthdaylem1  25788  birthday  25791  emcllem4  25835  emcllem6  25837  lgamgulmlem6  25870  basellem6  25922  ppiublem1  26037  bposlem6  26124  bposlem8  26126  lgslem4  26135  lgsdir2lem2  26161  selberglem1  26380  selberglem3  26382  selberg  26383  selbergs  26409  qdrng  26455  edgfndxnn  27037  structvtxvallem  27065  usgrexmpllem  27302  usgrexmpl  27305  uhgrspan1  27345  upgrres  27348  umgrres  27349  usgrres  27350  upgrres1  27355  umgrres1  27356  usgrres1  27357  fusgrfis  27372  cusgrres  27490  vtxdlfgrval  27527  vtxdusgr0edgnelALT  27538  umgr2v2e  27567  vtxdginducedm1lem1  27581  vtxdginducedm1fi  27586  finsumvtxdg2ssteplem4  27590  pthdlem1  27807  crctcshlem3  27857  2wlkd  27974  2wlkond  27975  2trlond  27977  2pthd  27978  2pthond  27980  umgr2adedgwlkonALT  27985  0pth  28162  wlk2v2e  28194  3wlkd  28207  3trlond  28210  3pthd  28211  3pthond  28212  3spthond  28214  eupthvdres  28272  eulerpathpr  28277  konigsbergumgr  28288  konigsberglem5  28293  konigsberg  28294  ex-lcm  28495  isvciOLD  28615  isnvi  28648  blocni  28840  hmoval  28845  cncph  28854  ipasslem7  28871  siilem2  28887  normlem2  29146  normlem3  29147  normlem6  29150  h0elch  29290  hhssabloilem  29296  hhsssh  29304  spansnji  29681  nonbooli  29686  3oalem5  29701  3oalem6  29702  3oai  29703  mayetes3i  29764  nmcexi  30061  nmbdfnlb  30085  rnelshi  30094  cnlnadjlem5  30106  pjbdlni  30184  golem2  30307  goeqi  30308  dp2clq  30829  rpdp2cl  30830  rpdp2cl2  30831  dpmul100  30845  rpdpcl  30851  xrge0tsmsd  30990  pmtrto1cl  31039  psgnfzto1stlem  31040  fzto1st  31043  psgnfzto1st  31045  nn0omnd  31213  xrge0slmod  31216  qusima  31262  prmidl0  31294  fply1  31335  ccfldextdgrr  31410  circtopn  31455  circcn  31456  zarcmplem  31499  tpr2tp  31522  tpr2rico  31530  ordtprsval  31536  ordtprsuni  31537  ordtrestNEW  31539  ordtrest2NEWlem  31540  ordtrest2NEW  31541  ordtconnlem1  31542  mndpluscn  31544  xrge0pluscn  31558  xrge0mulc1cn  31559  xrge0haus  31562  lmlimxrge0  31566  lmxrge0  31570  qqhcn  31607  qqhucn  31608  esumex  31663  esumcst  31697  hasheuni  31719  esumcvg  31720  prsiga  31765  brsiga  31817  mbfmcnt  31901  sxbrsigalem3  31905  dya2iocuni  31916  dya2iocucvr  31917  sxbrsigalem1  31918  sxbrsiga  31923  eulerpartlemt  32004  fibp1  32034  coinflipprob  32112  coinfliprv  32115  ccatmulgnn0dir  32187  signswplusg  32200  hgt750lem2  32298  hgt750leme  32304  bnj105  32369  bnj918  32412  bnj95  32511  bnj852  32568  bnj865  32570  subfacp1lem1  32808  subfacp1lem3  32811  subfacp1lem5  32813  subfacp1lem6  32814  kur14lem7  32841  iisconn  32881  iillysconn  32882  cvmliftlem5  32918  cvmliftlem8  32921  cvmliftlem10  32923  cvmlift2lem9  32940  satfv0  32987  goalrlem  33025  goalr  33026  satffunlem2lem2  33035  circum  33299  iexpire  33370  0sno  33706  1sno  33707  lrrecse  33785  altopex  33948  colinearex  34048  ssoninhaus  34323  cnndvlem2  34404  bj-pinftyccb  35076  taupi  35177  isbasisrelowl  35215  relowlpssretop  35221  poimirlem29  35492  poimirlem30  35493  poimirlem31  35494  dvasin  35547  dvacos  35548  areacirc  35556  upixp  35573  fdc  35589  lmclim2  35602  cncfres  35609  heibor1lem  35653  rrnval  35671  rrnmet  35673  reheibor  35683  isdrngo2  35802  isrngohom  35809  idlval  35857  isidl  35858  igenval  35905  scottexf  36012  cnvepresex  36155  renegclALT  36663  ldualfvadd  36828  cmtfvalN  36910  cvrfval  36968  cdleme31fv  38090  cdlemk40  38617  cdlemk56  38671  dibopelvalN  38843  dibopelval2  38845  dibelval3  38847  diblsmopel  38871  cdlemn11a  38907  dihopelvalcpre  38948  dihpN  39036  hlhilsca  39635  hlhilip  39648  3factsumint1  39712  lcmineqlem23  39742  aks4d1p1p6  39763  aks4d1p1p5  39765  acos1half  39833  sn-0tie0  40070  itrere  40085  retire  40086  prjspval  40091  flt4lem5e  40137  mapfzcons2  40185  jm2.23  40462  jm2.27dlem2  40476  jm2.27dlem4  40478  rmydioph  40480  rmxdioph  40482  expdiophlem2  40488  expdioph  40489  aomclem6  40528  pwslnmlem0  40560  frlmpwfi  40567  mncn0  40608  aaitgo  40631  arearect  40690  areaquad  40691  comptiunov2i  40932  frege110  41199  frege133  41222  scottex2  41477  radcnvrat  41546  uzmptshftfval  41578  dvradcnv2  41579  binomcxplemdvbinom  41585  binomcxplemcvg  41586  binomcxplemnotnn0  41588  rfcnpre1  42176  fcnre  42182  refsumcn  42187  refsum2cnlem1  42194  unirnmapsn  42368  infxrpnf  42601  iocopn  42674  icoopn  42679  mccl  42757  clim1fr1  42760  islptre  42778  sumnnodd  42789  lptre2pt  42799  limclner  42810  limclr  42814  expfac  42816  0cnf  43036  icccncfext  43046  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  itgsin0pilem1  43109  iblempty  43124  itgvol0  43127  stoweidlem47  43206  stoweidlem53  43212  stoweidlem57  43216  stoweidlem59  43218  wallispilem3  43226  wallispilem4  43227  wallispilem5  43228  wallispi  43229  stirlinglem1  43233  stirlinglem8  43240  stirlinglem12  43244  stirlinglem13  43245  stirlinglem14  43246  stirlinglem15  43247  dirkerper  43255  dirkercncflem2  43263  fourierdlem16  43282  fourierdlem21  43287  fourierdlem22  43288  fourierdlem36  43302  fourierdlem42  43308  fourierdlem71  43336  fourierdlem83  43348  fourierdlem102  43367  fourierdlem103  43368  fourierdlem104  43369  fourierdlem111  43376  fourierdlem112  43377  fourierdlem114  43379  sqwvfoura  43387  sqwvfourb  43388  fourierswlem  43389  fouriersw  43390  etransclem48  43441  salexct3  43499  salgencntex  43500  salgensscntex  43501  iooborel  43508  bor1sal  43512  gsumge0cl  43527  sge0tsms  43536  sge0isum  43583  nnfoctbdjlem  43611  isomenndlem  43686  mbfresmf  43890  incsmflem  43892  incsmf  43893  smfmbfcex  43910  decsmflem  43916  decsmf  43917  smflimlem1  43921  smfpimbor1lem2  43948  smf2id  43950  smfco  43951  smfpimcclem  43955  sprsymrelfolem1  44560  sprbisymrel  44567  fmtno0prm  44626  fmtno1prm  44627  fmtno2prm  44628  fmtno3prm  44630  fmtno4prm  44643  m2prm  44659  m3prm  44660  m5prm  44666  m7prm  44668  lighneallem4a  44676  0evenALTV  44756  1oddALTV  44758  2evenALTV  44760  6even  44779  7odd  44780  8even  44781  9gbo  44842  strisomgrop  44908  ushrisomgr  44909  uspgrex  44928  issubmgm2  44960  lmod1zrnlvec  45451  zlmodzxzldeplem1  45457  zlmodzxzldeplem3  45459  zlmodzxzldeplem4  45460  zlmodzxzldep  45461  ldepsnlinclem1  45462  ldepsnlinclem2  45463  blennn0elnn  45539  nn0sumshdiglemA  45581  nn0sumshdiglemB  45582  itcovalpclem2  45633  itcovalt2lem2  45638  ackval42  45658  rrx2line  45702  rrx2linesl  45705  spheres  45708  2sphere  45711  2sphere0  45712  line2x  45716  line2y  45717  functhinclem1  45938  prsthinc  45951