Theorem equcom 2022

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

Syntax hints:   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784

This theorem is referenced by:  equcomd  2023  dvelimhw  2345  nfeqf1  2379  eu1  2612  reu7  3662  reu8  3663  dfdif3  4045  issn  4760  iunid  4986  disjxun  5068  copsexgw  5398  copsexg  5399  dfid4  5481  dfid3  5483  opeliunxp  5645  dmi  5819  elidinxp  5940  opabresid  5946  opabresidOLD  5948  asymref2  6011  intirr  6012  cnvi  6034  coi1  6155  cnvso  6180  iotaval  6392  brprcneu  6747  fvprc  6748  dffv2  6845  fvn0ssdmfun  6934  f1oiso  7202  fvmpopr2d  7412  fsplit  7928  qsid  8530  mapsnend  8780  marypha2lem2  9125  fiinfg  9188  dfac5lem2  9811  dfac5lem3  9812  kmlem15  9851  brdom7disj  10218  suplem2pr  10740  wloglei  11437  fimaxre  11849  arch  12160  dflt2  12811  hashgt12el  14065  hashge2el2dif  14122  summo  15357  tosso  18052  opsrtoslem1  21172  mamulid  21498  mpomatmul  21503  mattpos1  21513  scmatscm  21570  1marepvmarrepid  21632  ist1-3  22408  unisngl  22586  fmid  23019  tgphaus  23176  dscopn  23635  iundisj2  24618  dvlip  25062  ply1divmo  25205  disjabrex  30822  disjabrexf  30823  iundisj2f  30830  iundisj2fi  31020  grplsm0l  31493  ordtconnlem1  31776  dfdm5  33653  dfrn5  33654  poxp2  33717  poxp3  33723  xpord3ind  33727  addsid1  34054  dffun10  34143  elfuns  34144  dfiota3  34152  brimg  34166  dfrdg4  34180  nn0prpwlem  34438  fvineqsneu  35509  wl-equsalcom  35628  matunitlindflem2  35701  pmapglb  37711  polval2N  37847  diclspsn  39135  sn-iotalem  40117  sn-iotaval  40119  eq0rabdioph  40514  ontric3g  41027  undmrnresiss  41101  relopabVD  42410  icheq  44802  ichexmpl1  44809  opeliun2xp  45556  itsclquadeu  46011