Theorem eqeltri 2824

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 2819	. 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 2701

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

This theorem is referenced by:  eqeltrri  2825  3eltr4i  2841  intab  4942  axrep6g  5245  unisn2  5267  inex2  5273  vpwex  5332  ord3ex  5342  zfpair  5376  vsnex  5389  opex  5424  otex  5425  uniopel  5476  elvvuni  5715  isarep2  6608  fvex  6871  fvexi  6872  riotaex  7348  ovexi  7421  tpex  7722  oprabex  7955  oprabrexex2  7957  mpoexw  8057  mptmpoopabbrd  8059  mptmpoopabbrdOLD  8060  tfrlem16  8361  1oex  8444  2oex  8445  1on  8446  2on  8447  3on  8450  4on  8451  oesuclem  8489  oecl  8501  o2p2e4  8505  nnecl  8577  1onnALT  8605  2onnALT  8607  3onn  8608  4onn  8609  mapsnf1o2  8867  sbthlem10  9060  cnvfi  9140  fnfi  9142  nnunifi  9238  imafiOLD  9265  pwfi  9268  xpfiOLD  9270  prfiALT  9275  tpfi  9276  fczfsuppd  9337  cantnfvalf  9618  oemapwe  9647  cantnffval2  9648  cnfcom3clem  9658  ssttrcl  9668  r1fin  9726  hta  9850  infxpenlem  9966  alephon  10022  alephfplem1  10057  dfac5lem4  10079  dfac5lem5  10080  dfac5lem4OLD  10081  kmlem10  10113  fin1a2lem10  10362  fin1a2lem12  10364  hsmexlem9  10378  axcc2lem  10389  domtriomlem  10395  axdc2lem  10401  axcclem  10410  brdom7disj  10484  brdom6disj  10485  iundom2g  10493  konigthlem  10521  canthwelem  10603  wunex2  10691  wunex3  10694  1nq  10881  1pr  10968  nrex1  11017  axcnex  11100  ax1cn  11102  pnfex  11227  mnfxr  11231  cju  12182  nnexALT  12188  2nn  12259  2re  12260  2cn  12261  3nn  12265  3re  12266  3cn  12267  4nn  12269  4re  12270  4cn  12271  5nn  12272  5re  12273  5cn  12274  6nn  12275  6re  12276  6cn  12277  7nn  12278  7re  12279  7cn  12280  8nn  12281  8re  12282  8cn  12283  9nn  12284  9re  12285  9cn  12286  nn0ex  12448  zexALT  12549  nneo  12618  zeo  12620  deccl  12664  10re  12668  decnncl  12669  numnncl2  12672  decnncl2  12673  numsucc  12689  numma2c  12695  numadd  12696  numaddc  12697  nummul1c  12698  nummul2c  12699  decmul1  12713  qexALT  12923  xrex  12946  xnegex  13168  xnegcl  13173  ixxssxr  13318  fz0to4untppr  13591  fz0to5un2tp  13592  om2uzuzi  13914  ltweuz  13926  axdc4uzlem  13948  seqex  13968  seqexw  13982  m1expcl2  14050  faccl  14248  facwordi  14254  faclbnd2  14256  bccl  14287  hashen1  14335  hashrabrsn  14337  hashunlei  14390  hashpw  14401  tpf1o  14466  s1cli  14570  ccat2s1p1  14594  cats1un  14686  revs1  14730  cshwsexa  14789  cshwsexaOLD  14790  cats1cli  14823  cats1fvn  14824  crre  15080  remim  15083  climmpt  15537  sumex  15654  supcvg  15822  geo2lim  15841  prodex  15871  bpoly4  16025  ere  16055  eftlub  16077  efsep  16078  tan0  16119  ef01bndlem  16152  nn0o  16353  divalglem5  16367  divalglem9  16371  sadcf  16423  smupf  16448  crth  16748  phimullem  16749  pczpre  16818  pockthi  16878  prmreclem2  16888  igz  16905  0ramcl  16994  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  strle1  17128  ndxarg  17166  basendxnn  17189  plusgndxnn  17248  tsetndxnn  17317  plendxnn  17331  dsndxnn  17350  unifndxnn  17360  prdsbasex  17413  prdsds  17427  yonedalem3  18241  isposix  18285  plusffval  18573  issubmgm2  18630  efmnd1hash  18819  efmnd2hash  18821  smndex1bas  18833  smndex1sgrp  18835  smndex1mnd  18837  smndex1id  18838  smndex2dbas  18841  smndex2hbas  18843  grpsubfval  18915  mulgfval  19001  symg1hash  19320  symg2hash  19322  symgvalstruct  19327  symgfisg  19398  psgnsn  19450  psgnprfval1  19452  odfval  19462  sylow2alem2  19548  efgsval2  19663  efgsp1  19667  pgpfaclem1  20013  dvdsrval  20270  isirred  20328  scaffval  20786  cnfldex  21267  xrsex  21294  pzriprnglem4  21394  pzriprnglem5  21395  pzriprnglem6  21396  pzriprng1ALT  21406  znle  21446  znidomb  21471  cnmsgnsubg  21486  refld  21528  ipffval  21557  psrbag0  21969  psrbagsn  21970  psr1baslem  22069  mat1dimbas  22359  mat1dimscm  22362  mat1f1o  22365  mat1rhmelval  22367  m2detleib  22518  pmatcoe1fsupp  22588  indistopon  22888  iccordt  23101  conncompid  23318  ptbasfi  23468  ptcmpfi  23700  ustfn  24089  ust0  24107  ustn0  24108  tmslem  24370  nmfval  24476  cnbl0  24661  cnopn  24674  remet  24678  re2ndc  24689  zcld  24702  icccmp  24714  xrge0gsumle  24722  xrge0tsms  24723  xmetdcn  24727  divcnOLD  24757  divcn  24759  expcn  24763  expcnOLD  24765  iiconn  24780  idcncf  24811  cnmpopc  24822  cnrehmeo  24851  cnrehmeoOLD  24852  cnheiborlem  24853  rellycmp  24856  bndth  24857  evth2  24859  cnrlmod  25043  cnrlvec  25044  cncmet  25222  ishl2  25270  ehleudis  25318  ehleudisval  25319  finiunmbl  25445  ioombl1lem4  25462  vitalilem4  25512  vitalilem5  25513  ismbf2d  25541  mbfimaopnlem  25556  mbfi1fseqlem6  25621  itgex  25671  bddmulibl  25740  ditgex  25753  recnperf  25806  dvcnvrelem2  25923  ftc1  25949  mdegcl  25974  plyeq0lem  26115  aaliou3lem4  26254  dvradcnv  26330  sincn  26354  coscn  26355  tanabsge  26415  circsubm  26462  reloggim  26508  logcn  26556  dvloglem  26557  logdmopn  26558  dvlog2  26562  2irrexpq  26640  cxpcn  26654  cxpcnOLD  26655  cxpcn3  26658  resqrtcn  26659  2logb9irrALT  26708  2irrexpqALT  26710  atanrecl  26821  atan1  26838  atansopn  26842  birthdaylem1  26861  birthday  26864  emcllem4  26909  emcllem6  26911  lgamgulmlem6  26944  basellem6  26996  ppiublem1  27113  bposlem6  27200  bposlem8  27202  lgslem4  27211  lgsdir2lem2  27237  selberglem1  27456  selberglem3  27458  selberg  27459  selbergs  27485  qdrng  27531  0sno  27738  1sno  27739  lrrecse  27849  precsexlem11  28119  seqsex  28179  nnsex  28211  n0sbday  28244  n0subs  28253  n0p1nns  28260  dfnns2  28261  zsex  28268  zs12ex  28338  edgfndxnn  28919  structvtxvallem  28947  usgrexmpllem  29187  usgrexmpl  29190  uhgrspan1  29230  upgrres  29233  umgrres  29234  usgrres  29235  upgrres1  29240  umgrres1  29241  usgrres1  29242  fusgrfis  29257  cusgrres  29376  vtxdlfgrval  29413  vtxdusgr0edgnelALT  29424  umgr2v2e  29453  vtxdginducedm1lem1  29467  vtxdginducedm1fi  29472  finsumvtxdg2ssteplem4  29476  pthdlem1  29696  crctcshlem3  29749  2wlkd  29866  2wlkond  29867  2trlond  29869  2pthd  29870  2pthond  29872  umgr2adedgwlkonALT  29877  0pth  30054  wlk2v2e  30086  3wlkd  30099  3trlond  30102  3pthd  30103  3pthond  30104  3spthond  30106  eupthvdres  30164  eulerpathpr  30169  konigsbergumgr  30180  konigsberglem5  30185  konigsberg  30186  ex-lcm  30387  isvciOLD  30509  isnvi  30542  blocni  30734  hmoval  30739  cncph  30748  ipasslem7  30765  siilem2  30781  normlem2  31040  normlem3  31041  normlem6  31044  h0elch  31184  hhssabloilem  31190  hhsssh  31198  spansnji  31575  nonbooli  31580  3oalem5  31595  3oalem6  31596  3oai  31597  mayetes3i  31658  nmcexi  31955  nmbdfnlb  31979  rnelshi  31988  cnlnadjlem5  32000  pjbdlni  32078  golem2  32201  goeqi  32202  dp2clq  32801  rpdp2cl  32802  rpdp2cl2  32803  dpmul100  32817  rpdpcl  32823  chnub  32938  xrge0tsmsd  33002  pmtrto1cl  33056  psgnfzto1stlem  33057  fzto1st  33060  psgnfzto1st  33062  nn0omnd  33316  xrge0slmod  33319  qusima  33379  prmidl0  33421  fply1  33527  ply1degltdimlem  33618  ccfldextdgrr  33667  algextdeglem8  33714  constrfin  33736  2sqr3minply  33770  2sqr3nconstr  33771  cos9thpiminplylem4  33775  cos9thpiminplylem5  33776  cos9thpinconstrlem2  33780  circtopn  33827  circcn  33828  zarcmplem  33871  tpr2tp  33894  tpr2rico  33902  ordtprsval  33908  ordtprsuni  33909  ordtrestNEW  33911  ordtrest2NEWlem  33912  ordtrest2NEW  33913  ordtconnlem1  33914  mndpluscn  33916  xrge0pluscn  33930  xrge0mulc1cn  33931  xrge0haus  33934  lmlimxrge0  33938  lmxrge0  33942  qqhcn  33981  qqhucn  33982  esumex  34019  esumcst  34053  hasheuni  34075  esumcvg  34076  prsiga  34121  brsiga  34173  mbfmcnt  34259  sxbrsigalem3  34263  dya2iocuni  34274  dya2iocucvr  34275  sxbrsigalem1  34276  sxbrsiga  34281  eulerpartlemt  34362  fibp1  34392  coinflipprob  34471  coinfliprv  34474  ccatmulgnn0dir  34533  signswplusg  34546  hgt750lem2  34643  hgt750leme  34649  bnj105  34714  bnj918  34756  bnj95  34854  bnj852  34911  bnj865  34913  subfacp1lem1  35166  subfacp1lem3  35169  subfacp1lem5  35171  subfacp1lem6  35172  kur14lem7  35199  iisconn  35239  iillysconn  35240  cvmliftlem5  35276  cvmliftlem8  35279  cvmliftlem10  35281  cvmlift2lem9  35298  satfv0  35345  goalrlem  35383  goalr  35384  satffunlem2lem2  35393  circum  35661  iexpire  35722  altopex  35948  colinearex  36048  ssoninhaus  36436  cnndvlem2  36526  bj-prex  37028  bj-prfromadj  37033  bj-pinftyccb  37209  taupi  37311  isbasisrelowl  37346  relowlpssretop  37352  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  dvasin  37698  dvacos  37699  areacirc  37707  upixp  37723  fdc  37739  lmclim2  37752  cncfres  37759  heibor1lem  37803  rrnval  37821  rrnmet  37823  reheibor  37833  isdrngo2  37952  isrngohom  37959  idlval  38007  isidl  38008  igenval  38055  scottexf  38162  cnvepresex  38318  renegclALT  38956  ldualfvadd  39121  cmtfvalN  39203  cvrfval  39261  cdleme31fv  40384  cdlemk40  40911  cdlemk56  40965  dibopelvalN  41137  dibopelval2  41139  dibelval3  41141  diblsmopel  41165  cdlemn11a  41201  dihopelvalcpre  41242  dihpN  41330  hlhilsca  41929  hlhilip  41942  3factsumint1  42009  lcmineqlem23  42039  aks4d1p1p6  42061  aks4d1p1p5  42063  aks6d1c6isolem2  42163  itrere  42306  acos1half  42346  redvmptabs  42348  readvrec2  42349  sn-0tie0  42439  sn-itrere  42476  sn-retire  42477  prjspval  42591  flt4lem5e  42644  sn-isghm  42661  mapfzcons2  42707  jm2.23  42985  jm2.27dlem2  42999  jm2.27dlem4  43001  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  expdioph  43012  aomclem6  43048  pwslnmlem0  43080  frlmpwfi  43087  mncn0  43128  aaitgo  43151  arearect  43204  areaquad  43205  omcl3g  43323  comptiunov2i  43695  frege110  43962  frege133  43985  scottex2  44234  radcnvrat  44303  uzmptshftfval  44335  dvradcnv2  44336  binomcxplemdvbinom  44342  binomcxplemcvg  44343  binomcxplemnotnn0  44345  permaxinf2lem  45002  rfcnpre1  45013  fcnre  45019  refsumcn  45024  refsum2cnlem1  45031  unirnmapsn  45208  infxrpnf  45442  iocopn  45518  icoopn  45523  mccl  45596  clim1fr1  45599  islptre  45617  sumnnodd  45628  lptre2pt  45638  limclner  45649  limclr  45653  expfac  45655  0cnf  45875  icccncfext  45885  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  itgsin0pilem1  45948  iblempty  45963  itgvol0  45966  stoweidlem47  46045  stoweidlem53  46051  stoweidlem57  46055  stoweidlem59  46057  wallispilem3  46065  wallispilem4  46066  wallispilem5  46067  wallispi  46068  stirlinglem1  46072  stirlinglem8  46079  stirlinglem12  46083  stirlinglem13  46084  stirlinglem14  46085  stirlinglem15  46086  dirkerper  46094  dirkercncflem2  46102  fourierdlem16  46121  fourierdlem21  46126  fourierdlem22  46127  fourierdlem36  46141  fourierdlem42  46147  fourierdlem71  46175  fourierdlem83  46187  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem112  46216  fourierdlem114  46218  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  etransclem48  46280  salexct3  46340  salgencntex  46341  salgensscntex  46342  iooborel  46349  bor1sal  46353  gsumge0cl  46369  sge0tsms  46378  sge0isum  46425  nnfoctbdjlem  46453  isomenndlem  46528  mbfresmf  46737  incsmflem  46739  incsmf  46740  smfmbfcex  46758  decsmflem  46764  decsmf  46765  smflimlem1  46769  smfpimbor1lem2  46797  smf2id  46799  smfco  46800  smfpimcclem  46805  tworepnotupword  46884  lambert0  46888  sprsymrelfolem1  47493  sprbisymrel  47500  fmtno0prm  47559  fmtno1prm  47560  fmtno2prm  47561  fmtno3prm  47563  fmtno4prm  47576  m2prm  47592  m3prm  47593  m5prm  47599  m7prm  47601  lighneallem4a  47609  0evenALTV  47689  1oddALTV  47691  2evenALTV  47693  6even  47712  7odd  47713  8even  47714  9gbo  47775  opstrgric  47926  ushggricedg  47927  grtri  47939  usgrexmpl1  48013  usgrexmpl1vtx  48014  usgrexmpl1edg  48015  usgrexmpl2  48018  usgrexmpl2vtx  48019  usgrexmpl2edg  48020  gpgprismgr4cycllem5  48089  pgnbgreunbgr  48115  pgn4cyclex  48116  uspgrex  48138  lmod1zrnlvec  48483  zlmodzxzldeplem1  48489  zlmodzxzldeplem3  48491  zlmodzxzldeplem4  48492  zlmodzxzldep  48493  ldepsnlinclem1  48494  ldepsnlinclem2  48495  blennn0elnn  48566  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  itcovalpclem2  48660  itcovalt2lem2  48665  ackval42  48685  rrx2line  48729  rrx2linesl  48732  spheres  48735  2sphere  48738  2sphere0  48739  line2x  48743  line2y  48744  resipos  48963  functhinclem1  49433  prsthinc  49453  setc1oterm  49480  funcsetc1ocl  49485  funcsetc1o  49486  isinito2lem  49487  isinito3  49489  functermc2  49498  incat  49590  setc1onsubc  49591