Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > disjxun | Structured version Visualization version Unicode version |
Description: The union of two disjoint collections. (Contributed by Mario Carneiro, 14-Nov-2016.) |
Ref | Expression |
---|---|
disjxun.1 |
Ref | Expression |
---|---|
disjxun | Disj Disj Disj |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | disjel 4023 | . . . . . . . . . . 11 | |
2 | eleq1 2689 | . . . . . . . . . . . 12 | |
3 | 2 | notbid 308 | . . . . . . . . . . 11 |
4 | 1, 3 | syl5ibcom 235 | . . . . . . . . . 10 |
5 | 4 | con2d 129 | . . . . . . . . 9 |
6 | 5 | impr 649 | . . . . . . . 8 |
7 | biorf 420 | . . . . . . . 8 | |
8 | 6, 7 | syl 17 | . . . . . . 7 |
9 | 8 | bicomd 213 | . . . . . 6 |
10 | 9 | 2ralbidva 2988 | . . . . 5 |
11 | 10 | anbi2d 740 | . . . 4 |
12 | ralunb 3794 | . . . . . 6 | |
13 | 12 | ralbii 2980 | . . . . 5 |
14 | nfv 1843 | . . . . . 6 | |
15 | nfcv 2764 | . . . . . . 7 | |
16 | nfv 1843 | . . . . . . . 8 | |
17 | nfcsb1v 3549 | . . . . . . . . . 10 | |
18 | nfcsb1v 3549 | . . . . . . . . . 10 | |
19 | 17, 18 | nfin 3820 | . . . . . . . . 9 |
20 | 19 | nfeq1 2778 | . . . . . . . 8 |
21 | 16, 20 | nfor 1834 | . . . . . . 7 |
22 | 15, 21 | nfral 2945 | . . . . . 6 |
23 | equequ2 1953 | . . . . . . . . 9 | |
24 | nfcv 2764 | . . . . . . . . . . . 12 | |
25 | nfcv 2764 | . . . . . . . . . . . 12 | |
26 | disjxun.1 | . . . . . . . . . . . 12 | |
27 | 24, 25, 26 | csbhypf 3552 | . . . . . . . . . . 11 |
28 | 27 | ineq2d 3814 | . . . . . . . . . 10 |
29 | 28 | eqeq1d 2624 | . . . . . . . . 9 |
30 | 23, 29 | orbi12d 746 | . . . . . . . 8 |
31 | 30 | cbvralv 3171 | . . . . . . 7 |
32 | equequ1 1952 | . . . . . . . . 9 | |
33 | csbeq1a 3542 | . . . . . . . . . . 11 | |
34 | 33 | ineq1d 3813 | . . . . . . . . . 10 |
35 | 34 | eqeq1d 2624 | . . . . . . . . 9 |
36 | 32, 35 | orbi12d 746 | . . . . . . . 8 |
37 | 36 | ralbidv 2986 | . . . . . . 7 |
38 | 31, 37 | syl5bbr 274 | . . . . . 6 |
39 | 14, 22, 38 | cbvral 3167 | . . . . 5 |
40 | r19.26 3064 | . . . . 5 | |
41 | 13, 39, 40 | 3bitr3i 290 | . . . 4 |
42 | 26 | disjor 4634 | . . . . 5 Disj |
43 | 42 | anbi1i 731 | . . . 4 Disj |
44 | 11, 41, 43 | 3bitr4g 303 | . . 3 Disj |
45 | nfv 1843 | . . . . . . . . . 10 | |
46 | equequ2 1953 | . . . . . . . . . . 11 | |
47 | csbeq1a 3542 | . . . . . . . . . . . . 13 | |
48 | 47 | ineq2d 3814 | . . . . . . . . . . . 12 |
49 | 48 | eqeq1d 2624 | . . . . . . . . . . 11 |
50 | 46, 49 | orbi12d 746 | . . . . . . . . . 10 |
51 | 45, 21, 50 | cbvral 3167 | . . . . . . . . 9 |
52 | equequ1 1952 | . . . . . . . . . . . 12 | |
53 | equcom 1945 | . . . . . . . . . . . 12 | |
54 | 52, 53 | syl6bb 276 | . . . . . . . . . . 11 |
55 | 24, 25, 26 | csbhypf 3552 | . . . . . . . . . . . . . 14 |
56 | 55 | ineq1d 3813 | . . . . . . . . . . . . 13 |
57 | incom 3805 | . . . . . . . . . . . . 13 | |
58 | 56, 57 | syl6eq 2672 | . . . . . . . . . . . 12 |
59 | 58 | eqeq1d 2624 | . . . . . . . . . . 11 |
60 | 54, 59 | orbi12d 746 | . . . . . . . . . 10 |
61 | 60 | ralbidv 2986 | . . . . . . . . 9 |
62 | 51, 61 | syl5bbr 274 | . . . . . . . 8 |
63 | 62 | cbvralv 3171 | . . . . . . 7 |
64 | ralcom 3098 | . . . . . . 7 | |
65 | 63, 64 | bitri 264 | . . . . . 6 |
66 | 65, 10 | syl5bb 272 | . . . . 5 |
67 | 66 | anbi1d 741 | . . . 4 |
68 | ralunb 3794 | . . . . . 6 | |
69 | 68 | ralbii 2980 | . . . . 5 |
70 | r19.26 3064 | . . . . 5 | |
71 | 69, 70 | bitri 264 | . . . 4 |
72 | disjors 4635 | . . . . 5 Disj | |
73 | 72 | anbi2ci 732 | . . . 4 Disj |
74 | 67, 71, 73 | 3bitr4g 303 | . . 3 Disj |
75 | 44, 74 | anbi12d 747 | . 2 Disj Disj |
76 | disjors 4635 | . . 3 Disj | |
77 | ralunb 3794 | . . 3 | |
78 | 76, 77 | bitri 264 | . 2 Disj |
79 | df-3an 1039 | . . 3 Disj Disj Disj Disj | |
80 | anandir 872 | . . 3 Disj Disj Disj Disj | |
81 | 79, 80 | bitri 264 | . 2 Disj Disj Disj Disj |
82 | 75, 78, 81 | 3bitr4g 303 | 1 Disj Disj Disj |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wb 196 wo 383 wa 384 w3a 1037 wceq 1483 wcel 1990 wral 2912 csb 3533 cun 3572 cin 3573 c0 3915 Disj wdisj 4620 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-nul 3916 df-disj 4621 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |