Theorem equcom 1732

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 1731	. 2 |- ( x = y -> y = x )
2		equcomi 1731	. 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 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728

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

This theorem is referenced by:  equequ2  1737  equvin  1742  dvelimhw  1881  nfeqf1  1991  eu1  2303  eu1OLD  2304  2eu6OLD  2371  reu7  3152  reu8  3153  iunid  4223  disjxun  4288  copsexg  4574  copsexgOLD  4575  opelopabsbALT  4596  dfid3  4635  opeliunxp  4888  relop  4988  dmi  5052  opabresid  5157  restidsing  5160  asymref2  5213  intirr  5214  cnvi  5239  coi1  5351  cnvso  5374  brprcneu  5682  dffv2  5762  f1oiso  6040  qsid  7164  mapsnen  7385  marypha2lem2  7684  dfac5lem2  8292  dfac5lem3  8293  kmlem15  8331  brdom7disj  8696  suplem2pr  9220  wloglei  9870  fimaxre  10275  arch  10574  dflt2  11123  hashgt12el  12171  hashge2el2dif  12182  summo  13192  tosso  15204  opsrtoslem1  17563  mamulid  18302  mattpos1  18338  1marepvmarrepid  18384  ist1-3  18951  cnmptid  19232  fmid  19531  tgphaus  19685  dscopn  20164  iundisj2  21028  dvlip  21463  ply1divmo  21605  disjabrex  25924  disjabrexf  25925  iundisj2f  25930  iundisj2fi  26079  ordtconlem1  26352  ghomf1olem  27311  dfid4  27380  dfdm5  27585  dfrn5  27586  dffun10  27943  elfuns  27944  dfiota3  27952  brimg  27966  dfrdg4  27979  wl-equsalcom  28368  nn0prpwlem  28514  eq0rabdioph  29112  frg2wot1  30647  opeliun2xp  30717  relopabVD  31634  bj-equcomd  32169  pmapglb  33411  polval2N  33547  diclspsn  34836