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  2374  sb8v  2382  sb8f  2383  nfeqf1  2408  eu1  2635  reu7  3690  reu8  3691  issn  4792  disjxun  5101  copsexgw  5466  copsexgwOLD  5467  copsexg  5468  dfid4  5551  dfid3  5553  opeliunxp  5722  opeliun2xp  5723  cnvi  5865  dmi  5905  elidinxp  6040  opabresid  6046  asymref2  6111  intirr  6112  coi1  6259  cnvso  6286  iotaval2  6504  brprcneu  6869  brprcneuALT  6870  dffv2  6974  fvn0ssdmfun  7068  f1oiso  7353  fvmpopr2d  7576  fsplit  8115  poxp2  8142  poxp3  8149  qsid  8782  mapsnend  9044  marypha2lem2  9407  fiinfg  9472  dfac5lem2  10128  dfac5lem3  10129  kmlem15  10168  brdom7disj  10535  suplem2pr  11063  wloglei  11771  fimaxre  12184  arch  12526  dflt2  13200  hashgt12el  14488  hashge2el2dif  14546  summo  15804  tosso  18506  opsrtoslem1  22272  mamulid  22664  mpomatmul  22669  mattpos1  22679  scmatscm  22736  1marepvmarrepid  22798  matunitlindflem2  22903  ist1-3  23575  unisngl  23754  fmid  24187  tgphaus  24344  dscopn  24800  iundisj2  25778  dvlip  26221  ply1divmo  26362  addsrid  28230  mulsrid  28379  disjabrex  33056  disjabrexf  33057  iundisj2f  33064  iundisj2fi  33269  grplsm0l  33833  esplyfvaln  34085  ordtconnlem1  34435  dfdm5  36353  dfrn5  36354  dffun10  36492  elfuns  36493  dfiota3  36501  brimg  36515  dfrdg4  36531  nn0prpwlem  36942  bj-axseprep  37820  fvineqsneu  38166  wl-equsalcom  38307  wl-sb9v  38313  ref5  39068  dfsucmap3  39212  pmapglb  40644  polval2N  40780  diclspsn  42068  sn-iotalem  43092  eq0rabdioph  43622  ontric3g  44363  undmrnresiss  44445  relopabVD  45724  icheq  48363  ichexmpl1  48370  pgnbgreunbgrlem4  49036  itsclquadeu  49708  oppcendc  49945