Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > un0 | Unicode version |
Description: The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
un0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | noel 3418 | . . . 4 | |
2 | 1 | biorfi 741 | . . 3 |
3 | 2 | bicomi 131 | . 2 |
4 | 3 | uneqri 3269 | 1 |
Colors of variables: wff set class |
Syntax hints: wo 703 wceq 1348 wcel 2141 cun 3119 c0 3414 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-v 2732 df-dif 3123 df-un 3125 df-nul 3415 |
This theorem is referenced by: un00 3461 disjssun 3478 difun2 3494 difdifdirss 3499 disjpr2 3647 prprc1 3691 diftpsn3 3721 iununir 3956 suc0 4396 sucprc 4397 fvun1 5562 fmptpr 5688 fvunsng 5690 fvsnun1 5693 fvsnun2 5694 fsnunfv 5697 fsnunres 5698 rdg0 6366 omv2 6444 unsnfidcex 6897 unfidisj 6899 undifdc 6901 ssfirab 6911 dju0en 7191 djuassen 7194 fzsuc2 10035 fseq1p1m1 10050 hashunlem 10739 ennnfonelem1 12362 setsresg 12454 setsslid 12466 fmelpw1o 13841 exmid1stab 14033 |
Copyright terms: Public domain | W3C validator |