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

Theorem equcom 1943
Description: Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.)
Assertion
Ref Expression
equcom (𝑥 = 𝑦𝑦 = 𝑥)

Proof of Theorem equcom
StepHypRef Expression
1 equcomi 1942 . 2 (𝑥 = 𝑦𝑦 = 𝑥)
2 equcomi 1942 . 2 (𝑦 = 𝑥𝑥 = 𝑦)
31, 2impbii 199 1 (𝑥 = 𝑦𝑦 = 𝑥)
Colors of variables: wff setvar class
Syntax hints:  wb 196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703
This theorem is referenced by:  equcomd  1944  equequ2OLD  1953  dvelimhw  2171  nfeqf1  2297  eu1  2508  reu7  3395  reu8  3396  issn  4354  iunid  4566  disjxun  4642  copsexg  4946  opelopabsbALT  4974  dfid3  5015  dfid4  5016  opeliunxp  5160  dmi  5329  opabresid  5443  restidsingOLD  5447  asymref2  5501  intirr  5502  cnvi  5525  coi1  5639  cnvso  5662  iotaval  5850  brprcneu  6171  dffv2  6258  fvn0ssdmfun  6336  f1oiso  6586  qsid  7798  mapsnen  8020  marypha2lem2  8327  fiinfg  8390  dfac5lem2  8932  dfac5lem3  8933  kmlem15  8971  brdom7disj  9338  suplem2pr  9860  wloglei  10545  fimaxre  10953  arch  11274  dflt2  11966  hashgt12el  13193  hashge2el2dif  13245  summo  14429  tosso  17017  opsrtoslem1  19465  mamulid  20228  mpt2matmul  20233  mattpos1  20243  scmatscm  20300  1marepvmarrepid  20362  ist1-3  21134  unisngl  21311  cnmptid  21445  fmid  21745  tgphaus  21901  dscopn  22359  iundisj2  23298  dvlip  23737  ply1divmo  23876  disjabrex  29367  disjabrexf  29368  iundisj2f  29375  iundisj2fi  29530  ordtconnlem1  29944  dfdm5  31650  dfrn5  31651  dffun10  31996  elfuns  31997  dfiota3  32005  brimg  32019  dfrdg4  32033  nn0prpwlem  32292  bj-ssbequ2  32618  wl-equsalcom  33299  matunitlindflem2  33377  pmapglb  34875  polval2N  35011  diclspsn  36302  eq0rabdioph  37159  undmrnresiss  37729  relopabVD  38957  mapsnend  39207  opeliun2xp  41876
  Copyright terms: Public domain W3C validator