Theorem equcom 1942

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 1941	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1941	. 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 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932

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

This theorem is referenced by:  equcomd  1943  equequ2OLD  1952  dvelimhw  2170  nfeqf1  2298  eu1  2509  reu7  3383  reu8  3384  issn  4331  iunid  4541  disjxun  4611  copsexg  4916  opelopabsbALT  4944  dfid3  4990  dfid4  4991  opeliunxp  5131  dmi  5300  opabresid  5414  restidsingOLD  5418  asymref2  5472  intirr  5473  cnvi  5496  coi1  5610  cnvso  5633  iotaval  5821  brprcneu  6141  dffv2  6228  fvn0ssdmfun  6306  f1oiso  6555  qsid  7758  mapsnen  7979  marypha2lem2  8286  fiinfg  8349  dfac5lem2  8891  dfac5lem3  8892  kmlem15  8930  brdom7disj  9297  suplem2pr  9819  wloglei  10504  fimaxre  10912  arch  11233  dflt2  11925  hashgt12el  13150  hashge2el2dif  13200  summo  14381  tosso  16957  opsrtoslem1  19403  mamulid  20166  mpt2matmul  20171  mattpos1  20181  scmatscm  20238  1marepvmarrepid  20300  ist1-3  21063  unisngl  21240  cnmptid  21374  fmid  21674  tgphaus  21830  dscopn  22288  iundisj2  23224  dvlip  23660  ply1divmo  23799  frgr2wwlk1  27052  disjabrex  29240  disjabrexf  29241  iundisj2f  29248  iundisj2fi  29397  ordtconnlem1  29752  dfdm5  31378  dfrn5  31379  dffun10  31663  elfuns  31664  dfiota3  31672  brimg  31686  dfrdg4  31700  nn0prpwlem  31959  bj-ssbequ2  32285  wl-equsalcom  32960  matunitlindflem2  33038  pmapglb  34536  polval2N  34672  diclspsn  35963  eq0rabdioph  36820  undmrnresiss  37391  relopabVD  38620  mapsnend  38865  opeliun2xp  41399