Theorem equcom 2019

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 2018	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 2018	. 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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

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

This theorem is referenced by:  equcomd  2020  dvelimhw  2345  sb8v  2353  sb8f  2354  nfeqf1  2379  eu1  2605  reu7  3686  reu8  3687  dfdif3OLD  4065  issn  4781  disjxun  5087  copsexgw  5428  copsexg  5429  dfid4  5510  dfid3  5512  opeliunxp  5681  opeliun2xp  5682  dmi  5860  elidinxp  5992  opabresid  5998  asymref2  6063  intirr  6064  cnvi  6088  coi1  6210  cnvso  6235  iotaval2  6452  brprcneu  6812  brprcneuALT  6813  dffv2  6917  fvn0ssdmfun  7007  f1oiso  7285  fvmpopr2d  7508  fsplit  8047  poxp2  8073  poxp3  8080  qsid  8705  mapsnend  8958  marypha2lem2  9320  fiinfg  9385  dfac5lem2  10015  dfac5lem3  10016  kmlem15  10056  brdom7disj  10422  suplem2pr  10944  wloglei  11649  fimaxre  12066  arch  12378  dflt2  13047  hashgt12el  14329  hashge2el2dif  14387  summo  15624  tosso  18323  opsrtoslem1  21990  mamulid  22356  mpomatmul  22361  mattpos1  22371  scmatscm  22428  1marepvmarrepid  22490  ist1-3  23264  unisngl  23442  fmid  23875  tgphaus  24032  dscopn  24488  iundisj2  25477  dvlip  25925  ply1divmo  26068  addsrid  27907  mulsrid  28052  disjabrex  32562  disjabrexf  32563  iundisj2f  32570  iundisj2fi  32779  grplsm0l  33368  ordtconnlem1  33937  dfdm5  35817  dfrn5  35818  dffun10  35956  elfuns  35957  dfiota3  35965  brimg  35979  dfrdg4  35995  nn0prpwlem  36366  fvineqsneu  37455  wl-equsalcom  37587  wl-sb9v  37593  matunitlindflem2  37667  ref5  38361  dfsucmap3  38486  pmapglb  39879  polval2N  40015  diclspsn  41303  sn-iotalem  42324  eq0rabdioph  42879  ontric3g  43625  undmrnresiss  43707  relopabVD  45003  icheq  47572  ichexmpl1  47579  pgnbgreunbgrlem4  48229  itsclquadeu  48888  oppcendc  49129