Theorem equcom 2017

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 2016	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 2016	. 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 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007

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

This theorem is referenced by:  equcomd  2018  dvelimhw  2351  sb8v  2358  sb8f  2359  nfeqf1  2387  eu1  2613  reu7  3754  reu8  3755  dfdif3OLD  4141  issn  4857  iunidOLD  5084  disjxun  5164  copsexgw  5510  copsexg  5511  dfid4  5594  dfid3  5596  opeliunxp  5767  dmi  5946  elidinxp  6073  opabresid  6079  asymref2  6149  intirr  6150  cnvi  6173  coi1  6293  cnvso  6319  iotaval2  6541  iotavalOLD  6547  brprcneu  6910  brprcneuALT  6911  dffv2  7017  fvn0ssdmfun  7108  f1oiso  7387  fvmpopr2d  7612  fsplit  8158  poxp2  8184  poxp3  8191  qsid  8841  mapsnend  9101  marypha2lem2  9505  fiinfg  9568  dfac5lem2  10193  dfac5lem3  10194  kmlem15  10234  brdom7disj  10600  suplem2pr  11122  wloglei  11822  fimaxre  12239  arch  12550  dflt2  13210  hashgt12el  14471  hashge2el2dif  14529  summo  15765  tosso  18489  opsrtoslem1  22102  mamulid  22468  mpomatmul  22473  mattpos1  22483  scmatscm  22540  1marepvmarrepid  22602  ist1-3  23378  unisngl  23556  fmid  23989  tgphaus  24146  dscopn  24607  iundisj2  25603  dvlip  26052  ply1divmo  26195  addsrid  28015  mulsrid  28157  disjabrex  32604  disjabrexf  32605  iundisj2f  32612  iundisj2fi  32802  grplsm0l  33396  ordtconnlem1  33870  dfdm5  35736  dfrn5  35737  dffun10  35878  elfuns  35879  dfiota3  35887  brimg  35901  dfrdg4  35915  nn0prpwlem  36288  fvineqsneu  37377  wl-equsalcom  37497  wl-sb9v  37503  matunitlindflem2  37577  ref5  38269  pmapglb  39727  polval2N  39863  diclspsn  41151  sn-iotalem  42214  eq0rabdioph  42732  ontric3g  43484  undmrnresiss  43566  relopabVD  44872  icheq  47336  ichexmpl1  47343  opeliun2xp  48057  itsclquadeu  48511