Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > disjsn | Unicode version |
Description: Intersection with the singleton of a non-member is disjoint. (Contributed by NM, 22-May-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Sep-2014.) |
Ref | Expression |
---|---|
disjsn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | disj1 3465 | . 2 | |
2 | con2b 664 | . . . 4 | |
3 | velsn 3600 | . . . . 5 | |
4 | 3 | imbi1i 237 | . . . 4 |
5 | imnan 685 | . . . 4 | |
6 | 2, 4, 5 | 3bitri 205 | . . 3 |
7 | 6 | albii 1463 | . 2 |
8 | alnex 1492 | . . 3 | |
9 | df-clel 2166 | . . 3 | |
10 | 8, 9 | xchbinxr 678 | . 2 |
11 | 1, 7, 10 | 3bitri 205 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wa 103 wb 104 wal 1346 wceq 1348 wex 1485 wcel 2141 cin 3120 c0 3414 csn 3583 |
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-fal 1354 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 df-v 2732 df-dif 3123 df-in 3127 df-nul 3415 df-sn 3589 |
This theorem is referenced by: disjsn2 3646 ssdifsn 3711 orddisj 4530 ndmima 4988 funtpg 5249 fnunsn 5305 ressnop0 5677 ftpg 5680 fsnunf 5696 fsnunfv 5697 enpr2d 6795 phpm 6843 fiunsnnn 6859 ac6sfi 6876 unsnfi 6896 tpfidisj 6905 iunfidisj 6923 pm54.43 7167 dju1en 7190 fzpreddisj 10027 fzp1disj 10036 frecfzennn 10382 hashunsng 10742 hashxp 10761 fsumsplitsn 11373 sumtp 11377 fsumsplitsnun 11382 fsum2dlemstep 11397 fsumconst 11417 fsumabs 11428 fsumiun 11440 fprodm1 11561 fprodunsn 11567 fprod2dlemstep 11585 fprodsplitsn 11596 ennnfonelemhf1o 12368 structcnvcnv 12432 fsumcncntop 13350 |
Copyright terms: Public domain | W3C validator |