Theorem equcom 1799

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 1798	. 2 |- ( x = y -> y = x )
2		equcomi 1798	. 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 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795

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

This theorem is referenced by:  equequ2  1804  equvin  1809  dvelimhw  1960  nfeqf1  2047  eu1  2328  2eu6OLD  2381  reu7  3291  reu8  3292  iunid  4370  disjxun  4437  copsexg  4722  opelopabsbALT  4745  dfid3  4785  opeliunxp  5040  relop  5142  dmi  5206  opabresid  5315  restidsing  5318  asymref2  5372  intirr  5373  cnvi  5395  coi1  5506  cnvso  5529  brprcneu  5841  dffv2  5921  fvn0ssdmfun  5998  f1oiso  6222  qsid  7369  mapsnen  7586  marypha2lem2  7888  dfac5lem2  8496  dfac5lem3  8497  kmlem15  8535  brdom7disj  8900  suplem2pr  9420  wloglei  10081  fimaxre  10485  arch  10788  dflt2  11357  hashgt12el  12465  hashge2el2dif  12505  summo  13621  tosso  15865  opsrtoslem1  18343  mamulid  19110  mpt2matmul  19115  mattpos1  19125  scmatscm  19182  1marepvmarrepid  19244  ist1-3  20017  unisngl  20194  cnmptid  20328  fmid  20627  tgphaus  20781  dscopn  21260  iundisj2  22125  dvlip  22560  ply1divmo  22702  frg2wot1  25259  disjabrex  27653  disjabrexf  27654  iundisj2f  27660  iundisj2fi  27836  ordtconlem1  28141  ghomf1olem  29298  dfid4  29344  dfdm5  29446  dfrn5  29447  dffun10  29792  elfuns  29793  dfiota3  29801  brimg  29815  dfrdg4  29828  wl-equsalcom  30235  nn0prpwlem  30380  eq0rabdioph  30949  opeliun2xp  33176  relopabVD  34102  bj-equcomd  34635  pmapglb  35891  polval2N  36027  diclspsn  37318