Theorem equcom 1743

Description: Commutative law for equality. (Contributed by NM, 20-Aug-1993.)

Assertion

Ref	Expression
equcom	|- ( x = y <-> y = x )

Proof of Theorem equcom

Step	Hyp	Ref	Expression
1		equcomi 1742	. 2 |- ( x = y -> y = x )
2		equcomi 1742	. 2 |- ( y = x -> x = y )
3	1, 2	impbii 188	1 |- ( x = y <-> y = x )

Syntax hints:   <-> wb 184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739

This theorem depends on definitions:  df-bi 185  df-ex 1597

This theorem is referenced by:  equequ2  1748  equvin  1753  dvelimhw  1902  nfeqf1  2016  eu1  2325  eu1OLD  2326  2eu6OLD  2394  reu7  3298  reu8  3299  iunid  4380  disjxun  4445  copsexg  4732  copsexgOLD  4733  opelopabsbALT  4756  dfid3  4796  opeliunxp  5051  relop  5153  dmi  5217  opabresid  5327  restidsing  5330  asymref2  5384  intirr  5385  cnvi  5410  coi1  5523  cnvso  5546  brprcneu  5859  dffv2  5940  f1oiso  6235  qsid  7377  mapsnen  7593  marypha2lem2  7896  dfac5lem2  8505  dfac5lem3  8506  kmlem15  8544  brdom7disj  8909  suplem2pr  9431  wloglei  10085  fimaxre  10490  arch  10792  dflt2  11354  hashgt12el  12446  hashge2el2dif  12487  summo  13502  tosso  15523  opsrtoslem1  17947  mamulid  18738  mattpos1  18753  scmatscm  18810  1marepvmarrepid  18872  ist1-3  19644  cnmptid  19925  fmid  20224  tgphaus  20378  dscopn  20857  iundisj2  21722  dvlip  22157  ply1divmo  22299  frg2wot1  24762  disjabrex  27144  disjabrexf  27145  iundisj2f  27150  iundisj2fi  27298  ordtconlem1  27570  ghomf1olem  28537  dfid4  28606  dfdm5  28811  dfrn5  28812  dffun10  29169  elfuns  29170  dfiota3  29178  brimg  29192  dfrdg4  29205  wl-equsalcom  29600  nn0prpwlem  29745  eq0rabdioph  30342  opeliun2xp  32018  relopabVD  32799  bj-equcomd  33336  pmapglb  34584  polval2N  34720  diclspsn  36009