Theorem equcom 2051

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  equcomd  2052  dvelimhw  2376  sb8v  2384  sb8f  2385  nfeqf1  2410  eu1  2637  reu7  3693  reu8  3694  issn  4795  disjxun  5105  copsexgw  5470  copsexgwOLD  5471  copsexg  5472  dfid4  5555  dfid3  5557  opeliunxp  5726  opeliun2xp  5727  cnvi  5869  dmi  5909  elidinxp  6044  opabresid  6050  asymref2  6115  intirr  6116  coi1  6263  cnvso  6290  iotaval2  6508  brprcneu  6872  brprcneuALT  6873  dffv2  6977  fvn0ssdmfun  7071  f1oiso  7356  fvmpopr2d  7579  fsplit  8118  poxp2  8145  poxp3  8152  qsid  8785  mapsnend  9047  marypha2lem2  9410  fiinfg  9475  dfac5lem2  10131  dfac5lem3  10132  kmlem15  10171  brdom7disj  10538  suplem2pr  11066  wloglei  11774  fimaxre  12187  arch  12529  dflt2  13203  hashgt12el  14491  hashge2el2dif  14549  summo  15807  tosso  18511  opsrtoslem1  22277  mamulid  22669  mpomatmul  22674  mattpos1  22684  scmatscm  22741  1marepvmarrepid  22803  matunitlindflem2  22908  ist1-3  23580  unisngl  23759  fmid  24192  tgphaus  24349  dscopn  24805  iundisj2  25783  dvlip  26227  ply1divmo  26368  addsrid  28237  mulsrid  28386  disjabrex  33063  disjabrexf  33064  iundisj2f  33071  iundisj2fi  33276  grplsm0l  33840  esplyfvaln  34092  ordtconnlem1  34442  dfdm5  36360  dfrn5  36361  dffun10  36499  elfuns  36500  dfiota3  36508  brimg  36522  dfrdg4  36538  nn0prpwlem  36949  bj-axseprep  37827  fvineqsneu  38173  wl-equsalcom  38314  wl-sb9v  38320  ref5  39075  dfsucmap3  39219  pmapglb  40651  polval2N  40787  diclspsn  42075  sn-iotalem  43099  eq0rabdioph  43629  ontric3g  44370  undmrnresiss  44452  relopabVD  45731  icheq  48370  ichexmpl1  48377  pgnbgreunbgrlem4  49043  itsclquadeu  49715  oppcendc  49952