Theorem equcom 1873

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

Syntax hints:   <-> wb 189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675

This theorem is referenced by:  equcomd  1874  equequ2  1879  equvin  1884  dvelimhw  2071  nfeqf1  2148  eu1  2350  reu7  3245  reu8  3246  iunid  4347  disjxun  4416  copsexg  4704  opelopabsbALT  4727  dfid3  4772  dfid4  4773  opeliunxp  4908  dmi  5071  opabresid  5180  restidsing  5183  asymref2  5239  intirr  5240  cnvi  5262  coi1  5374  cnvso  5398  brprcneu  5885  dffv2  5966  fvn0ssdmfun  6041  f1oiso  6272  qsid  7460  mapsnen  7678  marypha2lem2  7981  fiinfg  8046  dfac5lem2  8586  dfac5lem3  8587  kmlem15  8625  brdom7disj  8990  suplem2pr  9509  wloglei  10179  fimaxre  10584  arch  10900  dflt2  11481  hashgt12el  12634  hashge2el2dif  12676  summo  13838  tosso  16337  opsrtoslem1  18762  mamulid  19521  mpt2matmul  19526  mattpos1  19536  scmatscm  19593  1marepvmarrepid  19655  ist1-3  20420  unisngl  20597  cnmptid  20731  fmid  21030  tgphaus  21186  dscopn  21643  iundisj2  22558  dvlip  23001  ply1divmo  23142  frg2wot1  25841  disjabrex  28246  disjabrexf  28247  iundisj2f  28254  iundisj2fi  28425  ordtconlem1  28781  ghomf1olem  30362  dfdm5  30468  dfrn5  30469  dffun10  30731  elfuns  30732  dfiota3  30740  brimg  30754  dfrdg4  30768  nn0prpwlem  31028  bj-ssbequ2  31302  wl-equsalcom  31921  pmapglb  33381  polval2N  33517  diclspsn  34808  eq0rabdioph  35665  undmrnresiss  36256  relopabVD  37339  mapsnend  37534  issn  39132  opeliun2xp  40483