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

Theorem equcom 2115
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 2114 . 2 (𝑥 = 𝑦𝑦 = 𝑥)
2 equcomi 2114 . 2 (𝑦 = 𝑥𝑥 = 𝑦)
31, 2impbii 200 1 (𝑥 = 𝑦𝑦 = 𝑥)
Colors of variables: wff setvar class
Syntax hints:  wb 197
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875
This theorem is referenced by:  equcomd  2116  dvelimhw  2340  nfeqf1  2399  eu1  2631  reu7  3560  reu8  3561  dfdif3  3882  issn  4515  iunid  4731  disjxun  4807  copsexg  5111  opelopabsbALT  5145  dfid3  5186  dfid4  5187  opeliunxp  5338  dmi  5508  elidinxp  5632  opabresid  5639  asymref2  5696  intirr  5697  cnvi  5720  coi1  5837  cnvso  5860  iotaval  6042  brprcneu  6367  dffv2  6460  fvn0ssdmfun  6540  f1oiso  6793  qsid  8016  mapsnend  8239  marypha2lem2  8549  fiinfg  8612  dfac5lem2  9198  dfac5lem3  9199  kmlem15  9239  brdom7disj  9606  suplem2pr  10128  wloglei  10814  fimaxre  11222  arch  11535  dflt2  12181  hashgt12el  13411  hashge2el2dif  13463  summo  14733  tosso  17302  opsrtoslem1  19757  mamulid  20523  mpt2matmul  20529  mattpos1  20539  scmatscm  20596  1marepvmarrepid  20658  ist1-3  21433  unisngl  21610  cnmptid  21744  fmid  22043  tgphaus  22199  dscopn  22657  iundisj2  23607  dvlip  24047  ply1divmo  24186  disjabrex  29843  disjabrexf  29844  iundisj2f  29851  iundisj2fi  30005  ordtconnlem1  30417  dfdm5  32119  dfrn5  32120  dffun10  32465  elfuns  32466  dfiota3  32474  brimg  32488  dfrdg4  32502  nn0prpwlem  32760  bj-ssbequ2  33079  wl-equsalcom  33753  matunitlindflem2  33830  pmapglb  35726  polval2N  35862  diclspsn  37150  eq0rabdioph  38018  undmrnresiss  38585  relopabVD  39789  opeliun2xp  42780
  Copyright terms: Public domain W3C validator