![]() |
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 6346 dffv2 6434 fvn0ssdmfun 6514 f1oiso 6765 qsid 7982 mapsnen 8202 marypha2lem2 8509 fiinfg 8572 dfac5lem2 9157 dfac5lem3 9158 kmlem15 9198 brdom7disj 9565 suplem2pr 10087 wloglei 10772 fimaxre 11180 arch 11501 dflt2 12194 hashgt12el 13422 hashge2el2dif 13474 summo 14667 tosso 17257 opsrtoslem1 19706 mamulid 20469 mpt2matmul 20474 mattpos1 20484 scmatscm 20541 1marepvmarrepid 20603 ist1-3 21375 unisngl 21552 cnmptid 21686 fmid 21985 tgphaus 22141 dscopn 22599 iundisj2 23537 dvlip 23975 ply1divmo 24114 disjabrex 29723 disjabrexf 29724 iundisj2f 29731 iundisj2fi 29886 ordtconnlem1 30300 dfdm5 32002 dfrn5 32003 dffun10 32348 elfuns 32349 dfiota3 32357 brimg 32371 dfrdg4 32385 nn0prpwlem 32644 bj-ssbequ2 32971 wl-equsalcom 33659 matunitlindflem2 33737 pmapglb 35577 polval2N 35713 diclspsn 37003 eq0rabdioph 37860 undmrnresiss 38430 relopabVD 39654 mapsnend 39908 opeliun2xp 42639 |
Copyright terms: Public domain | W3C validator |