Theorem equcom 1945

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 1944	. 2 |- ( x = y -> y = x )
2		equcomi 1944	. 2 |- ( y = x -> x = y )
3	1, 2	impbii 199	1 |- ( x = y <-> y = x )

Syntax hints:   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  equcomd  1946  equequ2OLD  1955  dvelimhw  2173  nfeqf1  2299  eu1  2510  reu7  3401  reu8  3402  issn  4363  iunid  4575  disjxun  4651  copsexg  4956  opelopabsbALT  4984  dfid3  5025  dfid4  5026  opeliunxp  5170  dmi  5340  opabresid  5455  restidsingOLD  5459  asymref2  5513  intirr  5514  cnvi  5537  coi1  5651  cnvso  5674  iotaval  5862  brprcneu  6184  dffv2  6271  fvn0ssdmfun  6350  f1oiso  6601  qsid  7813  mapsnen  8035  marypha2lem2  8342  fiinfg  8405  dfac5lem2  8947  dfac5lem3  8948  kmlem15  8986  brdom7disj  9353  suplem2pr  9875  wloglei  10560  fimaxre  10968  arch  11289  dflt2  11981  hashgt12el  13210  hashge2el2dif  13262  summo  14448  tosso  17036  opsrtoslem1  19484  mamulid  20247  mpt2matmul  20252  mattpos1  20262  scmatscm  20319  1marepvmarrepid  20381  ist1-3  21153  unisngl  21330  cnmptid  21464  fmid  21764  tgphaus  21920  dscopn  22378  iundisj2  23317  dvlip  23756  ply1divmo  23895  disjabrex  29395  disjabrexf  29396  iundisj2f  29403  iundisj2fi  29556  ordtconnlem1  29970  dfdm5  31676  dfrn5  31677  dffun10  32021  elfuns  32022  dfiota3  32030  brimg  32044  dfrdg4  32058  nn0prpwlem  32317  bj-ssbequ2  32643  wl-equsalcom  33328  matunitlindflem2  33406  pmapglb  35056  polval2N  35192  diclspsn  36483  eq0rabdioph  37340  undmrnresiss  37910  relopabVD  39137  mapsnend  39391  opeliun2xp  42111