![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > equcom | Structured version Visualization version Unicode 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 1872 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | equcomi 1872 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbii 192 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1675 |
This theorem is referenced by: equcomd 1874 equequ2 1879 equvin 1884 dvelimhw 2071 nfeqf1 2148 eu1 2350 reu7 3245 reu8 3246 iunid 4347 disjxun 4416 copsexg 4704 opelopabsbALT 4727 dfid3 4772 dfid4 4773 opeliunxp 4908 dmi 5071 opabresid 5180 restidsing 5183 asymref2 5239 intirr 5240 cnvi 5262 coi1 5374 cnvso 5398 brprcneu 5885 dffv2 5966 fvn0ssdmfun 6041 f1oiso 6272 qsid 7460 mapsnen 7678 marypha2lem2 7981 fiinfg 8046 dfac5lem2 8586 dfac5lem3 8587 kmlem15 8625 brdom7disj 8990 suplem2pr 9509 wloglei 10179 fimaxre 10584 arch 10900 dflt2 11481 hashgt12el 12634 hashge2el2dif 12676 summo 13838 tosso 16337 opsrtoslem1 18762 mamulid 19521 mpt2matmul 19526 mattpos1 19536 scmatscm 19593 1marepvmarrepid 19655 ist1-3 20420 unisngl 20597 cnmptid 20731 fmid 21030 tgphaus 21186 dscopn 21643 iundisj2 22558 dvlip 23001 ply1divmo 23142 frg2wot1 25841 disjabrex 28246 disjabrexf 28247 iundisj2f 28254 iundisj2fi 28425 ordtconlem1 28781 ghomf1olem 30362 dfdm5 30468 dfrn5 30469 dffun10 30731 elfuns 30732 dfiota3 30740 brimg 30754 dfrdg4 30768 nn0prpwlem 31028 bj-ssbequ2 31302 wl-equsalcom 31921 pmapglb 33381 polval2N 33517 diclspsn 34808 eq0rabdioph 35665 undmrnresiss 36256 relopabVD 37339 mapsnend 37534 issn 39132 opeliun2xp 40483 |
Copyright terms: Public domain | W3C validator |