Theorem eqeltri 2833

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

Syntax hints:   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  eqeltrri  2834  3eltr4i  2850  intab  4921  axrep6g  5225  unisn2  5247  inex2  5255  vpwex  5314  ord3ex  5324  zfpair  5358  vsnex  5372  snex  5376  opex  5411  opexOLD  5412  otex  5413  uniopel  5464  elvvuni  5701  isarep2  6582  fvex  6847  fvexi  6848  riotaex  7321  ovexi  7394  tpex  7693  oprabex  7922  oprabrexex2  7924  mpoexw  8024  mptmpoopabbrd  8026  tfrlem16  8325  1oex  8408  2oex  8409  1on  8410  2on  8411  3on  8414  4on  8415  oesuclem  8453  oecl  8465  o2p2e4  8469  nnecl  8542  1onnALT  8570  2onnALT  8572  3onn  8573  4onn  8574  mapsnf1o2  8835  sbthlem10  9027  cnvfi  9103  fnfi  9105  nnunifi  9194  imafiOLD  9219  pwfi  9222  prfiALT  9228  tpfi  9229  fczfsuppd  9292  cantnfvalf  9577  oemapwe  9606  cantnffval2  9607  cnfcom3clem  9617  ssttrcl  9627  r1fin  9688  hta  9812  infxpenlem  9926  alephon  9982  alephfplem1  10017  dfac5lem4  10039  dfac5lem5  10040  dfac5lem4OLD  10041  kmlem10  10073  fin1a2lem10  10322  fin1a2lem12  10324  hsmexlem9  10338  axcc2lem  10349  domtriomlem  10355  axdc2lem  10361  axcclem  10370  brdom7disj  10444  brdom6disj  10445  iundom2g  10453  konigthlem  10482  canthwelem  10564  wunex2  10652  wunex3  10655  1nq  10842  1pr  10929  nrex1  10978  axcnex  11061  ax1cn  11063  pnfex  11189  mnfxr  11193  cju  12146  nnexALT  12167  2nn  12245  2re  12246  2cn  12247  3nn  12251  3re  12252  3cn  12253  4nn  12255  4re  12256  4cn  12257  5nn  12258  5re  12259  5cn  12260  6nn  12261  6re  12262  6cn  12263  7nn  12264  7re  12265  7cn  12266  8nn  12267  8re  12268  8cn  12269  9nn  12270  9re  12271  9cn  12272  nn0ex  12434  zexALT  12535  nneo  12604  zeo  12606  deccl  12650  10re  12654  decnncl  12655  numnncl2  12658  decnncl2  12659  numsucc  12675  numma2c  12681  numadd  12682  numaddc  12683  nummul1c  12684  nummul2c  12685  decmul1  12699  qexALT  12905  xrex  12928  xnegex  13151  xnegcl  13156  ixxssxr  13301  fz0to4untppr  13575  fz0to5un2tp  13576  om2uzuzi  13902  ltweuz  13914  axdc4uzlem  13936  seqex  13956  seqexw  13970  m1expcl2  14038  faccl  14236  facwordi  14242  faclbnd2  14244  bccl  14275  hashen1  14323  hashrabrsn  14325  hashunlei  14378  hashpw  14389  tpf1o  14454  s1cli  14559  ccat2s1p1  14583  cats1un  14674  revs1  14718  cshwsexa  14777  cats1cli  14810  cats1fvn  14811  crre  15067  remim  15070  climmpt  15524  sumex  15641  supcvg  15812  geo2lim  15831  prodex  15861  bpoly4  16015  ere  16045  eftlub  16067  efsep  16068  tan0  16109  ef01bndlem  16142  nn0o  16343  divalglem5  16357  divalglem9  16361  sadcf  16413  smupf  16438  crth  16739  phimullem  16740  pczpre  16809  pockthi  16869  prmreclem2  16879  igz  16896  0ramcl  16985  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  1259prm  17097  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  4001prm  17106  strle1  17119  ndxarg  17157  basendxnn  17180  plusgndxnn  17239  tsetndxnn  17308  plendxnn  17322  dsndxnn  17341  unifndxnn  17351  prdsbasex  17404  prdsds  17418  yonedalem3  18237  isposix  18281  chnub  18579  plusffval  18605  issubmgm2  18662  efmnd1hash  18851  efmnd2hash  18853  smndex1bas  18868  smndex1sgrp  18870  smndex1mnd  18872  smndex1id  18873  smndex2dbas  18876  smndex2hbas  18878  grpsubfval  18950  mulgfval  19036  symg1hash  19356  symg2hash  19358  symgvalstruct  19363  symgfisg  19434  psgnsn  19486  psgnprfval1  19488  odfval  19498  sylow2alem2  19584  efgsval2  19699  efgsp1  19703  pgpfaclem1  20049  dvdsrval  20332  isirred  20390  scaffval  20866  cnfldex  21347  xrsex  21374  pzriprnglem4  21474  pzriprnglem5  21475  pzriprnglem6  21476  pzriprng1ALT  21486  znle  21526  znidomb  21551  cnmsgnsubg  21567  refld  21609  ipffval  21638  psrbag0  22050  psrbagsn  22051  psr1baslem  22158  mat1dimbas  22447  mat1dimscm  22450  mat1f1o  22453  mat1rhmelval  22455  m2detleib  22606  pmatcoe1fsupp  22676  indistopon  22976  iccordt  23189  conncompid  23406  ptbasfi  23556  ptcmpfi  23788  ustfn  24177  ust0  24195  ustn0  24196  tmslem  24457  nmfval  24563  cnbl0  24748  cnopn  24761  remet  24765  re2ndc  24776  zcld  24789  icccmp  24801  xrge0gsumle  24809  xrge0tsms  24810  xmetdcn  24814  divcn  24845  expcn  24849  iiconn  24864  idcncf  24895  cnmpopc  24905  cnrehmeo  24930  cnheiborlem  24931  rellycmp  24934  bndth  24935  evth2  24937  cnrlmod  25120  cnrlvec  25121  cncmet  25299  ishl2  25347  ehleudis  25395  ehleudisval  25396  finiunmbl  25521  ioombl1lem4  25538  vitalilem4  25588  vitalilem5  25589  ismbf2d  25617  mbfimaopnlem  25632  mbfi1fseqlem6  25697  itgex  25747  bddmulibl  25816  ditgex  25829  recnperf  25882  dvcnvrelem2  25995  ftc1  26019  mdegcl  26044  plyeq0lem  26185  aaliou3lem4  26323  dvradcnv  26399  sincn  26422  coscn  26423  tanabsge  26483  circsubm  26530  reloggim  26576  logcn  26624  dvloglem  26625  logdmopn  26626  dvlog2  26630  2irrexpq  26708  cxpcn  26722  cxpcn3  26725  resqrtcn  26726  2logb9irrALT  26775  2irrexpqALT  26777  atanrecl  26888  atan1  26905  atansopn  26909  birthdaylem1  26928  birthday  26931  emcllem4  26976  emcllem6  26978  lgamgulmlem6  27011  basellem6  27063  ppiublem1  27179  bposlem6  27266  bposlem8  27268  lgslem4  27277  lgsdir2lem2  27303  selberglem1  27522  selberglem3  27524  selberg  27525  selbergs  27551  qdrng  27597  0no  27815  1no  27816  lrrecse  27948  precsexlem11  28223  seqsex  28291  nnsex  28324  n0bday  28358  n0subs  28369  n0p1nns  28377  dfnns2  28378  zsex  28386  bdayfinbndlem1  28473  z12sex  28480  z12shalf  28486  edgfndxnn  29075  structvtxvallem  29103  usgrexmpllem  29343  usgrexmpl  29346  uhgrspan1  29386  upgrres  29389  umgrres  29390  usgrres  29391  upgrres1  29396  umgrres1  29397  usgrres1  29398  fusgrfis  29413  cusgrres  29532  vtxdlfgrval  29569  vtxdusgr0edgnelALT  29580  umgr2v2e  29609  vtxdginducedm1lem1  29623  vtxdginducedm1fi  29628  finsumvtxdg2ssteplem4  29632  pthdlem1  29849  crctcshlem3  29902  2wlkd  30019  2wlkond  30020  2trlond  30022  2pthd  30023  2pthond  30025  umgr2adedgwlkonALT  30030  0pth  30210  wlk2v2e  30242  3wlkd  30255  3trlond  30258  3pthd  30259  3pthond  30260  3spthond  30262  eupthvdres  30320  eulerpathpr  30325  konigsbergumgr  30336  konigsberglem5  30341  konigsberg  30342  ex-lcm  30543  isvciOLD  30666  isnvi  30699  blocni  30891  hmoval  30896  cncph  30905  ipasslem7  30922  siilem2  30938  normlem2  31197  normlem3  31198  normlem6  31201  h0elch  31341  hhssabloilem  31347  hhsssh  31355  spansnji  31732  nonbooli  31737  3oalem5  31752  3oalem6  31753  3oai  31754  mayetes3i  31815  nmcexi  32112  nmbdfnlb  32136  rnelshi  32145  cnlnadjlem5  32157  pjbdlni  32235  golem2  32358  goeqi  32359  dp2clq  32955  rpdp2cl  32956  rpdp2cl2  32957  dpmul100  32971  rpdpcl  32977  xrge0tsmsd  33149  pmtrto1cl  33175  psgnfzto1stlem  33176  fzto1st  33179  psgnfzto1st  33181  nn0omnd  33419  xrge0slmod  33423  qusima  33483  prmidl0  33525  fply1  33633  extvfvcl  33695  ply1degltdimlem  33782  ccfldextdgrr  33832  algextdeglem8  33884  constrfin  33906  2sqr3minply  33940  2sqr3nconstr  33941  cos9thpiminplylem4  33945  cos9thpiminplylem5  33946  cos9thpinconstrlem2  33950  circtopn  33997  circcn  33998  zarcmplem  34041  tpr2tp  34064  tpr2rico  34072  ordtprsval  34078  ordtprsuni  34079  ordtrestNEW  34081  ordtrest2NEWlem  34082  ordtrest2NEW  34083  ordtconnlem1  34084  mndpluscn  34086  xrge0pluscn  34100  xrge0mulc1cn  34101  xrge0haus  34104  lmlimxrge0  34108  lmxrge0  34112  qqhcn  34151  qqhucn  34152  esumex  34189  esumcst  34223  hasheuni  34245  esumcvg  34246  prsiga  34291  brsiga  34343  mbfmcnt  34428  sxbrsigalem3  34432  dya2iocuni  34443  dya2iocucvr  34444  sxbrsigalem1  34445  sxbrsiga  34450  eulerpartlemt  34531  fibp1  34561  coinflipprob  34640  coinfliprv  34643  ccatmulgnn0dir  34702  signswplusg  34715  hgt750lem2  34812  hgt750leme  34818  bnj105  34883  bnj918  34925  bnj95  35022  bnj852  35079  bnj865  35081  fineqvnttrclse  35284  subfacp1lem1  35377  subfacp1lem3  35380  subfacp1lem5  35382  subfacp1lem6  35383  kur14lem7  35410  iisconn  35450  iillysconn  35451  cvmliftlem5  35487  cvmliftlem8  35490  cvmliftlem10  35492  cvmlift2lem9  35509  satfv0  35556  goalrlem  35594  goalr  35595  satffunlem2lem2  35604  circum  35872  iexpire  35933  altopex  36158  colinearex  36258  ssoninhaus  36646  cnndvlem2  36814  bj-prex  37363  bj-prfromadj  37368  bj-pinftyccb  37551  taupi  37653  isbasisrelowl  37688  relowlpssretop  37694  poimirlem29  37984  poimirlem30  37985  poimirlem31  37986  dvasin  38039  dvacos  38040  areacirc  38048  upixp  38064  fdc  38080  lmclim2  38093  cncfres  38100  heibor1lem  38144  rrnval  38162  rrnmet  38164  reheibor  38174  isdrngo2  38293  isrngohom  38300  idlval  38348  isidl  38349  igenval  38396  scottexf  38503  cnvepresex  38671  preex  38827  renegclALT  39423  ldualfvadd  39588  cmtfvalN  39670  cvrfval  39728  cdleme31fv  40850  cdlemk40  41377  cdlemk56  41431  dibopelvalN  41603  dibopelval2  41605  dibelval3  41607  diblsmopel  41631  cdlemn11a  41667  dihopelvalcpre  41708  dihpN  41796  hlhilsca  42395  hlhilip  42408  3factsumint1  42474  lcmineqlem23  42504  aks4d1p1p6  42526  aks4d1p1p5  42528  aks6d1c6isolem2  42628  itrere  42764  acos1half  42804  redvmptabs  42806  readvrec2  42807  sn-0tie0  42910  sn-itrere  42947  sn-retire  42948  prjspval  43050  flt4lem5e  43103  sn-isghm  43120  mapfzcons2  43165  jm2.23  43442  jm2.27dlem2  43456  jm2.27dlem4  43458  rmydioph  43460  rmxdioph  43462  expdiophlem2  43468  expdioph  43469  aomclem6  43505  pwslnmlem0  43537  frlmpwfi  43544  mncn0  43585  aaitgo  43608  arearect  43661  areaquad  43662  omcl3g  43780  comptiunov2i  44151  frege110  44418  frege133  44441  scottex2  44690  radcnvrat  44759  uzmptshftfval  44791  dvradcnv2  44792  binomcxplemdvbinom  44798  binomcxplemcvg  44799  binomcxplemnotnn0  44801  permaxinf2lem  45457  rfcnpre1  45468  fcnre  45474  refsumcn  45479  refsum2cnlem1  45486  unirnmapsn  45661  infxrpnf  45892  iocopn  45968  icoopn  45973  mccl  46046  clim1fr1  46049  islptre  46067  sumnnodd  46078  lptre2pt  46086  limclner  46097  limclr  46101  expfac  46103  0cnf  46323  icccncfext  46333  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  itgsin0pilem1  46396  iblempty  46411  itgvol0  46414  stoweidlem47  46493  stoweidlem53  46499  stoweidlem57  46503  stoweidlem59  46505  wallispilem3  46513  wallispilem4  46514  wallispilem5  46515  wallispi  46516  stirlinglem1  46520  stirlinglem8  46527  stirlinglem12  46531  stirlinglem13  46532  stirlinglem14  46533  stirlinglem15  46534  dirkerper  46542  dirkercncflem2  46550  fourierdlem16  46569  fourierdlem21  46574  fourierdlem22  46575  fourierdlem36  46589  fourierdlem42  46595  fourierdlem71  46623  fourierdlem83  46635  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fourierdlem112  46664  fourierdlem114  46666  sqwvfoura  46674  sqwvfourb  46675  fourierswlem  46676  fouriersw  46677  etransclem48  46728  salexct3  46788  salgencntex  46789  salgensscntex  46790  iooborel  46797  bor1sal  46801  gsumge0cl  46817  sge0tsms  46826  sge0isum  46873  nnfoctbdjlem  46901  isomenndlem  46976  mbfresmf  47185  incsmflem  47187  incsmf  47188  smfmbfcex  47206  decsmflem  47212  decsmf  47213  smflimlem1  47217  smfpimbor1lem2  47245  smf2id  47247  smfco  47248  smfpimcclem  47253  goldrarr  47343  lambert0  47347  sprsymrelfolem1  47964  sprbisymrel  47971  fmtno0prm  48033  fmtno1prm  48034  fmtno2prm  48035  fmtno3prm  48037  fmtno4prm  48050  m2prm  48066  m3prm  48067  m5prm  48073  m7prm  48075  lighneallem4a  48083  nprmdvdsfacm1lem4  48098  0evenALTV  48176  1oddALTV  48178  2evenALTV  48180  6even  48199  7odd  48200  8even  48201  9gbo  48262  opstrgric  48414  ushggricedg  48415  grtri  48428  usgrexmpl1  48510  usgrexmpl1vtx  48511  usgrexmpl1edg  48512  usgrexmpl2  48515  usgrexmpl2vtx  48516  usgrexmpl2edg  48517  gpgprismgr4cycllem5  48587  pgnbgreunbgr  48613  pgn4cyclex  48614  uspgrex  48638  lmod1zrnlvec  48982  zlmodzxzldeplem1  48988  zlmodzxzldeplem3  48990  zlmodzxzldeplem4  48991  zlmodzxzldep  48992  ldepsnlinclem1  48993  ldepsnlinclem2  48994  blennn0elnn  49065  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108  itcovalpclem2  49159  itcovalt2lem2  49164  ackval42  49184  rrx2line  49228  rrx2linesl  49231  spheres  49234  2sphere  49237  2sphere0  49238  line2x  49242  line2y  49243  resipos  49462  functhinclem1  49931  prsthinc  49951  setc1oterm  49978  funcsetc1ocl  49983  funcsetc1o  49984  isinito2lem  49985  isinito3  49987  functermc2  49996  incat  50088  setc1onsubc  50089