![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > unidm | Structured version Unicode version |
Description: Idempotent law for union of classes. Theorem 23 of [Suppes] p. 27. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
unidm |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oridm 514 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | uneqri 3593 |
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 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2599 df-v 3067 df-un 3428 |
This theorem is referenced by: unundi 3612 unundir 3613 uneqin 3696 difabs 3709 undifabs 3851 dfif5 3900 dfsn2 3985 diftpsn3 4107 unisn 4201 dfdm2 5464 unixpid 5467 fun2 5671 resasplit 5676 xpider 7268 pm54.43 8268 lefld 15495 symg2bas 16002 gsumzaddlem 16509 pwssplit1 17243 plyun0 21778 constr3trllem3 23670 sseqf 26906 probun 26933 filnetlem3 28736 mapfzcons 29187 diophin 29246 pwssplit4 29577 fiuneneq 29697 compne 29831 |
Copyright terms: Public domain | W3C validator |