![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > equcom | Structured version Visualization version GIF version |
Description: Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.) |
Ref | Expression |
---|---|
equcom | ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equcomi 2099 | . 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) | |
2 | equcomi 2099 | . 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦) | |
3 | 1, 2 | impbii 199 | 1 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1854 |
This theorem is referenced by: equcomd 2101 dvelimhw 2318 nfeqf1 2444 eu1 2648 reu7 3542 reu8 3543 dfdif3 3863 issn 4508 iunid 4727 disjxun 4802 copsexg 5104 opelopabsbALT 5134 dfid3 5175 dfid4 5176 opeliunxp 5327 dmi 5495 opabresid 5613 restidsingOLD 5617 asymref2 5671 intirr 5672 cnvi 5695 coi1 5812 cnvso 5835 iotaval 6023 brprcneu 6345 dffv2 6433 fvn0ssdmfun 6513 f1oiso 6764 qsid 7980 mapsnen 8200 marypha2lem2 8507 fiinfg 8570 dfac5lem2 9137 dfac5lem3 9138 kmlem15 9178 brdom7disj 9545 suplem2pr 10067 wloglei 10752 fimaxre 11160 arch 11481 dflt2 12174 hashgt12el 13402 hashge2el2dif 13454 summo 14647 tosso 17237 opsrtoslem1 19686 mamulid 20449 mpt2matmul 20454 mattpos1 20464 scmatscm 20521 1marepvmarrepid 20583 ist1-3 21355 unisngl 21532 cnmptid 21666 fmid 21965 tgphaus 22121 dscopn 22579 iundisj2 23517 dvlip 23955 ply1divmo 24094 disjabrex 29702 disjabrexf 29703 iundisj2f 29710 iundisj2fi 29865 ordtconnlem1 30279 dfdm5 31981 dfrn5 31982 dffun10 32327 elfuns 32328 dfiota3 32336 brimg 32350 dfrdg4 32364 nn0prpwlem 32623 bj-ssbequ2 32949 wl-equsalcom 33641 matunitlindflem2 33719 pmapglb 35559 polval2N 35695 diclspsn 36985 eq0rabdioph 37842 undmrnresiss 38412 relopabVD 39636 mapsnend 39890 opeliun2xp 42621 |
Copyright terms: Public domain | W3C validator |