![]() |
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 2021 | . 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) | |
2 | equcomi 2021 | . 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦) | |
3 | 1, 2 | impbii 208 | 1 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 |
This theorem is referenced by: equcomd 2023 dvelimhw 2342 sb8v 2349 sb8f 2350 nfeqf1 2379 eu1 2607 reu7 3727 reu8 3728 dfdif3 4113 issn 4832 iunidOLD 5063 disjxun 5145 copsexgw 5489 copsexg 5490 dfid4 5574 dfid3 5576 opeliunxp 5741 dmi 5919 elidinxp 6041 opabresid 6047 asymref2 6115 intirr 6116 cnvi 6138 coi1 6258 cnvso 6284 iotaval2 6508 iotavalOLD 6514 brprcneu 6878 brprcneuALT 6879 dffv2 6982 fvn0ssdmfun 7072 f1oiso 7343 fvmpopr2d 7564 fsplit 8098 poxp2 8124 poxp3 8131 qsid 8773 mapsnend 9032 marypha2lem2 9427 fiinfg 9490 dfac5lem2 10115 dfac5lem3 10116 kmlem15 10155 brdom7disj 10522 suplem2pr 11044 wloglei 11742 fimaxre 12154 arch 12465 dflt2 13123 hashgt12el 14378 hashge2el2dif 14437 summo 15659 tosso 18368 opsrtoslem1 21598 mamulid 21925 mpomatmul 21930 mattpos1 21940 scmatscm 21997 1marepvmarrepid 22059 ist1-3 22835 unisngl 23013 fmid 23446 tgphaus 23603 dscopn 24064 iundisj2 25048 dvlip 25492 ply1divmo 25635 addsrid 27428 mulsrid 27549 disjabrex 31791 disjabrexf 31792 iundisj2f 31799 iundisj2fi 31986 grplsm0l 32478 ordtconnlem1 32842 dfdm5 34682 dfrn5 34683 dffun10 34824 elfuns 34825 dfiota3 34833 brimg 34847 dfrdg4 34861 nn0prpwlem 35145 fvineqsneu 36230 wl-equsalcom 36349 matunitlindflem2 36423 ref5 37120 pmapglb 38579 polval2N 38715 diclspsn 40003 sn-iotalem 40986 eq0rabdioph 41447 ontric3g 42206 undmrnresiss 42288 relopabVD 43595 icheq 46065 ichexmpl1 46072 opeliun2xp 46910 itsclquadeu 47365 |
Copyright terms: Public domain | W3C validator |