Theorem equcom 1848

Description: Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.)

Assertion

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

Proof of Theorem equcom

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

Syntax hints:   <-> wb 187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843

This theorem depends on definitions:  df-bi 188  df-ex 1658

This theorem is referenced by:  equequ2  1853  equvin  1858  dvelimhw  2037  nfeqf1  2109  eu1  2316  reu7  3208  reu8  3209  iunid  4297  disjxun  4364  copsexg  4649  opelopabsbALT  4672  dfid3  4712  dfid4  4713  opeliunxp  4848  relop  4947  dmi  5011  opabresid  5120  restidsing  5123  asymref2  5179  intirr  5180  cnvi  5202  coi1  5313  cnvso  5337  brprcneu  5818  dffv2  5898  fvn0ssdmfun  5972  f1oiso  6201  qsid  7384  mapsnen  7601  marypha2lem2  7903  fiinfg  7968  dfac5lem2  8506  dfac5lem3  8507  kmlem15  8545  brdom7disj  8910  suplem2pr  9429  wloglei  10097  fimaxre  10502  arch  10817  dflt2  11398  hashgt12el  12543  hashge2el2dif  12585  summo  13726  tosso  16225  opsrtoslem1  18650  mamulid  19408  mpt2matmul  19413  mattpos1  19423  scmatscm  19480  1marepvmarrepid  19542  ist1-3  20307  unisngl  20484  cnmptid  20618  fmid  20917  tgphaus  21073  dscopn  21530  iundisj2  22444  dvlip  22887  ply1divmo  23028  frg2wot1  25727  disjabrex  28138  disjabrexf  28139  iundisj2f  28146  iundisj2fi  28323  ordtconlem1  28682  ghomf1olem  30264  dfdm5  30369  dfrn5  30370  dffun10  30630  elfuns  30631  dfiota3  30639  brimg  30653  dfrdg4  30667  nn0prpwlem  30927  bj-equcomd  31179  wl-equsalcom  31782  pmapglb  33247  polval2N  33383  diclspsn  34674  eq0rabdioph  35531  undmrnresiss  36123  relopabVD  37214  issn  38804  opeliun2xp  39707