Theorem equcom 1943

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

Assertion

Ref	Expression
equcom	⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

Proof of Theorem equcom

Step	Hyp	Ref	Expression
1		equcomi 1942	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1942	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
3	1, 2	impbii 199	1 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

Syntax hints:   ↔ wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933

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

This theorem is referenced by:  equcomd  1944  equequ2OLD  1953  dvelimhw  2171  nfeqf1  2297  eu1  2508  reu7  3395  reu8  3396  issn  4354  iunid  4566  disjxun  4642  copsexg  4946  opelopabsbALT  4974  dfid3  5015  dfid4  5016  opeliunxp  5160  dmi  5329  opabresid  5443  restidsingOLD  5447  asymref2  5501  intirr  5502  cnvi  5525  coi1  5639  cnvso  5662  iotaval  5850  brprcneu  6171  dffv2  6258  fvn0ssdmfun  6336  f1oiso  6586  qsid  7798  mapsnen  8020  marypha2lem2  8327  fiinfg  8390  dfac5lem2  8932  dfac5lem3  8933  kmlem15  8971  brdom7disj  9338  suplem2pr  9860  wloglei  10545  fimaxre  10953  arch  11274  dflt2  11966  hashgt12el  13193  hashge2el2dif  13245  summo  14429  tosso  17017  opsrtoslem1  19465  mamulid  20228  mpt2matmul  20233  mattpos1  20243  scmatscm  20300  1marepvmarrepid  20362  ist1-3  21134  unisngl  21311  cnmptid  21445  fmid  21745  tgphaus  21901  dscopn  22359  iundisj2  23298  dvlip  23737  ply1divmo  23876  disjabrex  29367  disjabrexf  29368  iundisj2f  29375  iundisj2fi  29530  ordtconnlem1  29944  dfdm5  31650  dfrn5  31651  dffun10  31996  elfuns  31997  dfiota3  32005  brimg  32019  dfrdg4  32033  nn0prpwlem  32292  bj-ssbequ2  32618  wl-equsalcom  33299  matunitlindflem2  33377  pmapglb  34875  polval2N  35011  diclspsn  36302  eq0rabdioph  37159  undmrnresiss  37729  relopabVD  38957  mapsnend  39207  opeliun2xp  41876