Theorem equcom 2018

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 2017	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 2017	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
3	1, 2	impbii 209	1 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

Syntax hints:   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780

This theorem is referenced by:  equcomd  2019  dvelimhw  2347  sb8v  2355  sb8f  2356  nfeqf1  2384  eu1  2610  reu7  3720  reu8  3721  dfdif3OLD  4098  issn  4813  iunidOLD  5042  disjxun  5122  copsexgw  5470  copsexg  5471  dfid4  5554  dfid3  5556  opeliunxp  5726  opeliun2xp  5727  dmi  5906  elidinxp  6036  opabresid  6042  asymref2  6111  intirr  6112  cnvi  6135  coi1  6256  cnvso  6282  iotaval2  6504  iotavalOLD  6510  brprcneu  6871  brprcneuALT  6872  dffv2  6979  fvn0ssdmfun  7069  f1oiso  7349  fvmpopr2d  7574  fsplit  8121  poxp2  8147  poxp3  8154  qsid  8802  mapsnend  9055  marypha2lem2  9453  fiinfg  9518  dfac5lem2  10143  dfac5lem3  10144  kmlem15  10184  brdom7disj  10550  suplem2pr  11072  wloglei  11774  fimaxre  12191  arch  12503  dflt2  13169  hashgt12el  14445  hashge2el2dif  14503  summo  15738  tosso  18434  opsrtoslem1  22018  mamulid  22384  mpomatmul  22389  mattpos1  22399  scmatscm  22456  1marepvmarrepid  22518  ist1-3  23292  unisngl  23470  fmid  23903  tgphaus  24060  dscopn  24517  iundisj2  25507  dvlip  25955  ply1divmo  26098  addsrid  27928  mulsrid  28073  disjabrex  32568  disjabrexf  32569  iundisj2f  32576  iundisj2fi  32779  grplsm0l  33423  ordtconnlem1  33960  dfdm5  35795  dfrn5  35796  dffun10  35937  elfuns  35938  dfiota3  35946  brimg  35960  dfrdg4  35974  nn0prpwlem  36345  fvineqsneu  37434  wl-equsalcom  37566  wl-sb9v  37572  matunitlindflem2  37646  ref5  38336  pmapglb  39794  polval2N  39930  diclspsn  41218  sn-iotalem  42239  eq0rabdioph  42774  ontric3g  43521  undmrnresiss  43603  relopabVD  44900  icheq  47456  ichexmpl1  47463  itsclquadeu  48737  oppcendc  48973