MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeltri Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 eqeltri.2 . 2 𝐵𝐶
2 eqeltri.1 . . 3 𝐴 = 𝐵
32eleq1i 2827 . 2 (𝐴𝐶𝐵𝐶)
41, 3mpbir 230 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539  wcel 2104
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728  df-clel 2814
This theorem is referenced by:  eqeltrri  2834  3eltr4i  2850  intab  4916  axrep6g  5226  unisn2  5245  inex2  5251  vpwex  5309  ord3ex  5319  zfpair  5353  opex  5392  otex  5393  uniopel  5443  elvvuni  5674  isarep2  6554  fvex  6817  fvexi  6818  riotaex  7268  ovexi  7341  tpex  7629  oprabex  7851  oprabrexex2  7853  mpoexw  7951  mptmpoopabbrd  7953  tfrlem16  8255  1oex  8338  2oex  8339  1on  8340  1onOLD  8341  2on  8342  2onOLD  8343  3on  8345  4on  8346  2oexOLD  8348  oesuclem  8386  oecl  8398  o2p2e4  8402  nnecl  8475  1onnALT  8502  2onnALT  8504  3onn  8505  4onn  8506  mapsnf1o2  8713  sbthlem10  8917  imafi  8996  pwfi  8999  cnvfi  9001  fnfi  9002  nnunifi  9109  xpfi  9129  prfi  9133  tpfi  9134  pwfiOLD  9158  fczfsuppd  9190  cantnfvalf  9467  oemapwe  9496  cantnffval2  9497  cnfcom3clem  9507  ssttrcl  9517  r1fin  9575  hta  9699  infxpenlem  9815  alephon  9871  alephfplem1  9906  dfac5lem4  9928  dfac5lem5  9929  kmlem10  9961  fin1a2lem10  10211  fin1a2lem12  10213  hsmexlem9  10227  axcc2lem  10238  domtriomlem  10244  axdc2lem  10250  axcclem  10259  brdom7disj  10333  brdom6disj  10334  iundom2g  10342  konigthlem  10370  canthwelem  10452  wunex2  10540  wunex3  10543  1nq  10730  1pr  10817  nrex1  10866  axcnex  10949  ax1cn  10951  pnfex  11074  mnfxr  11078  inelr  12009  cju  12015  nnexALT  12021  2nn  12092  2re  12093  2cn  12094  3nn  12098  3re  12099  3cn  12100  4nn  12102  4re  12103  4cn  12104  5nn  12105  5re  12106  5cn  12107  6nn  12108  6re  12109  6cn  12110  7nn  12111  7re  12112  7cn  12113  8nn  12114  8re  12115  8cn  12116  9nn  12117  9re  12118  9cn  12119  nn0ex  12285  zexALT  12385  nneo  12450  zeo  12452  deccl  12498  10re  12502  decnncl  12503  numnncl2  12506  decnncl2  12507  numsucc  12523  numma2c  12529  numadd  12530  numaddc  12531  nummul1c  12532  nummul2c  12533  decmul1  12547  qexALT  12750  xrex  12773  xnegex  12988  xnegcl  12993  ixxssxr  13137  om2uzuzi  13715  ltweuz  13727  axdc4uzlem  13749  seqex  13769  seqexw  13783  m1expcl2  13850  faccl  14043  facwordi  14049  faclbnd2  14051  bccl  14082  hashen1  14130  hashrabrsn  14132  hashunlei  14185  hashpw  14196  s1cli  14355  ccat2s1p1  14381  cats1un  14479  revs1  14523  cshwsexa  14582  cats1cli  14615  cats1fvn  14616  crre  14870  remim  14873  climmpt  15325  sumex  15444  supcvg  15613  geo2lim  15632  prodex  15662  bpoly4  15814  ere  15843  eftlub  15863  efsep  15864  tan0  15905  ef01bndlem  15938  nn0o  16137  divalglem5  16151  divalglem9  16155  sadcf  16205  smupf  16230  crth  16524  phimullem  16525  pczpre  16593  pockthi  16653  prmreclem2  16663  igz  16680  0ramcl  16769  1259lem1  16877  1259lem2  16878  1259lem3  16879  1259lem4  16880  1259lem5  16881  1259prm  16882  2503lem1  16883  2503lem2  16884  2503lem3  16885  2503prm  16886  4001lem1  16887  4001lem2  16888  4001lem3  16889  4001lem4  16890  4001prm  16891  strle1  16904  ndxarg  16942  basendxnn  16967  basendxnnOLD  16968  plusgndxnn  17035  tsetndxnn  17109  plendxnn  17123  dsndxnn  17142  unifndxnn  17152  prdsbasex  17206  prdsds  17220  yonedalem3  18043  isposix  18088  isposixOLD  18089  plusffval  18377  efmnd1hash  18576  efmnd2hash  18578  smndex1bas  18590  smndex1sgrp  18592  smndex1mnd  18594  smndex1id  18595  smndex2dbas  18598  smndex2hbas  18600  grpsubfval  18668  mulgfval  18747  symg1hash  19042  symg2hash  19044  symgvalstruct  19049  symgvalstructOLD  19050  symgfisg  19121  psgnsn  19173  psgnprfval1  19175  odfval  19185  sylow2alem2  19268  efgsval2  19384  efgsp1  19388  pgpfaclem1  19729  dvdsrval  19932  isirred  19986  scaffval  20186  xrsex  20658  zlmlemOLD  20764  znle  20785  znidomb  20814  cnmsgnsubg  20827  refld  20869  ipffval  20898  psrbag0  21315  psrbagsn  21316  psr1baslem  21401  mat1dimbas  21666  mat1dimscm  21669  mat1f1o  21672  mat1rhmelval  21674  m2detleib  21825  pmatcoe1fsupp  21895  indistopon  22196  iccordt  22410  conncompid  22627  ptbasfi  22777  ptcmpfi  23009  ustfn  23398  ust0  23416  ustn0  23417  tmslem  23682  tmslemOLD  23683  nmfval  23789  tnglemOLD  23842  cnbl0  23982  cnopn  23995  remet  23998  re2ndc  24009  zcld  24021  icccmp  24033  xrge0gsumle  24041  xrge0tsms  24042  xmetdcn  24046  divcn  24076  expcn  24080  iiconn  24095  idcncf  24126  cnmpopc  24136  cnrehmeo  24161  cnheiborlem  24162  rellycmp  24165  bndth  24166  evth2  24168  cnrlmod  24351  cnrlvec  24352  cncmet  24531  ishl2  24579  ehleudis  24627  ehleudisval  24628  finiunmbl  24753  ioombl1lem4  24770  vitalilem4  24820  vitalilem5  24821  ismbf2d  24849  mbfimaopnlem  24864  mbfi1fseqlem6  24930  itgex  24980  bddmulibl  25048  ditgex  25061  recnperf  25114  dvcnvrelem2  25227  ftc1  25251  mdegcl  25279  plyeq0lem  25416  aaliou3lem4  25551  dvradcnv  25625  sincn  25648  coscn  25649  tanabsge  25708  circsubm  25754  reloggim  25799  logcn  25847  dvloglem  25848  logdmopn  25849  dvlog2  25853  2irrexpq  25930  cxpcn  25943  cxpcn3  25946  resqrtcn  25947  2logb9irrALT  25993  2irrexpqALT  25995  atanrecl  26106  atan1  26123  atansopn  26127  birthdaylem1  26146  birthday  26149  emcllem4  26193  emcllem6  26195  lgamgulmlem6  26228  basellem6  26280  ppiublem1  26395  bposlem6  26482  bposlem8  26484  lgslem4  26493  lgsdir2lem2  26519  selberglem1  26738  selberglem3  26740  selberg  26741  selbergs  26767  qdrng  26813  edgfndxnn  27405  structvtxvallem  27435  usgrexmpllem  27672  usgrexmpl  27675  uhgrspan1  27715  upgrres  27718  umgrres  27719  usgrres  27720  upgrres1  27725  umgrres1  27726  usgrres1  27727  fusgrfis  27742  cusgrres  27860  vtxdlfgrval  27897  vtxdusgr0edgnelALT  27908  umgr2v2e  27937  vtxdginducedm1lem1  27951  vtxdginducedm1fi  27956  finsumvtxdg2ssteplem4  27960  pthdlem1  28179  crctcshlem3  28229  2wlkd  28346  2wlkond  28347  2trlond  28349  2pthd  28350  2pthond  28352  umgr2adedgwlkonALT  28357  0pth  28534  wlk2v2e  28566  3wlkd  28579  3trlond  28582  3pthd  28583  3pthond  28584  3spthond  28586  eupthvdres  28644  eulerpathpr  28649  konigsbergumgr  28660  konigsberglem5  28665  konigsberg  28666  ex-lcm  28867  isvciOLD  28987  isnvi  29020  blocni  29212  hmoval  29217  cncph  29226  ipasslem7  29243  siilem2  29259  normlem2  29518  normlem3  29519  normlem6  29522  h0elch  29662  hhssabloilem  29668  hhsssh  29676  spansnji  30053  nonbooli  30058  3oalem5  30073  3oalem6  30074  3oai  30075  mayetes3i  30136  nmcexi  30433  nmbdfnlb  30457  rnelshi  30466  cnlnadjlem5  30478  pjbdlni  30556  golem2  30679  goeqi  30680  dp2clq  31200  rpdp2cl  31201  rpdp2cl2  31202  dpmul100  31216  rpdpcl  31222  xrge0tsmsd  31362  pmtrto1cl  31411  psgnfzto1stlem  31412  fzto1st  31415  psgnfzto1st  31417  nn0omnd  31590  xrge0slmod  31593  qusima  31639  prmidl0  31671  fply1  31712  ccfldextdgrr  31787  circtopn  31832  circcn  31833  zarcmplem  31876  tpr2tp  31899  tpr2rico  31907  ordtprsval  31913  ordtprsuni  31914  ordtrestNEW  31916  ordtrest2NEWlem  31917  ordtrest2NEW  31918  ordtconnlem1  31919  mndpluscn  31921  xrge0pluscn  31935  xrge0mulc1cn  31936  xrge0haus  31939  lmlimxrge0  31943  lmxrge0  31947  qqhcn  31986  qqhucn  31987  esumex  32042  esumcst  32076  hasheuni  32098  esumcvg  32099  prsiga  32144  brsiga  32196  mbfmcnt  32280  sxbrsigalem3  32284  dya2iocuni  32295  dya2iocucvr  32296  sxbrsigalem1  32297  sxbrsiga  32302  eulerpartlemt  32383  fibp1  32413  coinflipprob  32491  coinfliprv  32494  ccatmulgnn0dir  32566  signswplusg  32579  hgt750lem2  32677  hgt750leme  32683  bnj105  32748  bnj918  32791  bnj95  32889  bnj852  32946  bnj865  32948  subfacp1lem1  33186  subfacp1lem3  33189  subfacp1lem5  33191  subfacp1lem6  33192  kur14lem7  33219  iisconn  33259  iillysconn  33260  cvmliftlem5  33296  cvmliftlem8  33299  cvmliftlem10  33301  cvmlift2lem9  33318  satfv0  33365  goalrlem  33403  goalr  33404  satffunlem2lem2  33413  circum  33677  iexpire  33746  0sno  34065  1sno  34066  lrrecse  34144  altopex  34307  colinearex  34407  ssoninhaus  34682  cnndvlem2  34763  bj-pinftyccb  35436  taupi  35538  isbasisrelowl  35573  relowlpssretop  35579  poimirlem29  35850  poimirlem30  35851  poimirlem31  35852  dvasin  35905  dvacos  35906  areacirc  35914  upixp  35931  fdc  35947  lmclim2  35960  cncfres  35967  heibor1lem  36011  rrnval  36029  rrnmet  36031  reheibor  36041  isdrngo2  36160  isrngohom  36167  idlval  36215  isidl  36216  igenval  36263  scottexf  36370  cnvepresex  36511  renegclALT  37019  ldualfvadd  37184  cmtfvalN  37266  cvrfval  37324  cdleme31fv  38446  cdlemk40  38973  cdlemk56  39027  dibopelvalN  39199  dibopelval2  39201  dibelval3  39203  diblsmopel  39227  cdlemn11a  39263  dihopelvalcpre  39304  dihpN  39392  hlhilsca  39991  hlhilip  40008  3factsumint1  40071  lcmineqlem23  40101  aks4d1p1p6  40123  aks4d1p1p5  40125  acos1half  40212  sn-0tie0  40458  itrere  40473  retire  40474  prjspval  40479  flt4lem5e  40530  mapfzcons2  40578  jm2.23  40856  jm2.27dlem2  40870  jm2.27dlem4  40872  rmydioph  40874  rmxdioph  40876  expdiophlem2  40882  expdioph  40883  aomclem6  40922  pwslnmlem0  40954  frlmpwfi  40961  mncn0  41002  aaitgo  41025  arearect  41084  areaquad  41085  comptiunov2i  41352  frege110  41619  frege133  41642  scottex2  41901  radcnvrat  41970  uzmptshftfval  42002  dvradcnv2  42003  binomcxplemdvbinom  42009  binomcxplemcvg  42010  binomcxplemnotnn0  42012  rfcnpre1  42600  fcnre  42606  refsumcn  42611  refsum2cnlem1  42618  unirnmapsn  42798  infxrpnf  43034  iocopn  43107  icoopn  43112  mccl  43188  clim1fr1  43191  islptre  43209  sumnnodd  43220  lptre2pt  43230  limclner  43241  limclr  43245  expfac  43247  0cnf  43467  icccncfext  43477  ioodvbdlimc1lem2  43522  ioodvbdlimc2lem  43524  itgsin0pilem1  43540  iblempty  43555  itgvol0  43558  stoweidlem47  43637  stoweidlem53  43643  stoweidlem57  43647  stoweidlem59  43649  wallispilem3  43657  wallispilem4  43658  wallispilem5  43659  wallispi  43660  stirlinglem1  43664  stirlinglem8  43671  stirlinglem12  43675  stirlinglem13  43676  stirlinglem14  43677  stirlinglem15  43678  dirkerper  43686  dirkercncflem2  43694  fourierdlem16  43713  fourierdlem21  43718  fourierdlem22  43719  fourierdlem36  43733  fourierdlem42  43739  fourierdlem71  43767  fourierdlem83  43779  fourierdlem102  43798  fourierdlem103  43799  fourierdlem104  43800  fourierdlem111  43807  fourierdlem112  43808  fourierdlem114  43810  sqwvfoura  43818  sqwvfourb  43819  fourierswlem  43820  fouriersw  43821  etransclem48  43872  salexct3  43930  salgencntex  43931  salgensscntex  43932  iooborel  43939  bor1sal  43943  gsumge0cl  43959  sge0tsms  43968  sge0isum  44015  nnfoctbdjlem  44043  isomenndlem  44118  mbfresmf  44327  incsmflem  44329  incsmf  44330  smfmbfcex  44348  decsmflem  44354  decsmf  44355  smflimlem1  44359  smfpimbor1lem2  44387  smf2id  44389  smfco  44390  smfpimcclem  44394  sprsymrelfolem1  45002  sprbisymrel  45009  fmtno0prm  45068  fmtno1prm  45069  fmtno2prm  45070  fmtno3prm  45072  fmtno4prm  45085  m2prm  45101  m3prm  45102  m5prm  45108  m7prm  45110  lighneallem4a  45118  0evenALTV  45198  1oddALTV  45200  2evenALTV  45202  6even  45221  7odd  45222  8even  45223  9gbo  45284  strisomgrop  45350  ushrisomgr  45351  uspgrex  45370  issubmgm2  45402  lmod1zrnlvec  45893  zlmodzxzldeplem1  45899  zlmodzxzldeplem3  45901  zlmodzxzldeplem4  45902  zlmodzxzldep  45903  ldepsnlinclem1  45904  ldepsnlinclem2  45905  blennn0elnn  45981  nn0sumshdiglemA  46023  nn0sumshdiglemB  46024  itcovalpclem2  46075  itcovalt2lem2  46080  ackval42  46100  rrx2line  46144  rrx2linesl  46147  spheres  46150  2sphere  46153  2sphere0  46154  line2x  46158  line2y  46159  functhinclem1  46380  prsthinc  46393  tworepnotupword  46579
  Copyright terms: Public domain W3C validator