Step | Hyp | Ref
| Expression |
1 | | nfdisj1 4633 |
. . . 4
Disj |
2 | | nfcv 2764 |
. . . . 5
|
3 | | disjabrexf.1 |
. . . . . . . . . . 11
|
4 | 3 | nfcri 2758 |
. . . . . . . . . 10
|
5 | | nfcsb1v 3549 |
. . . . . . . . . . 11
|
6 | 5 | nfcri 2758 |
. . . . . . . . . 10
|
7 | 4, 6 | nfan 1828 |
. . . . . . . . 9
|
8 | 7 | nfab 2769 |
. . . . . . . 8
|
9 | 8 | nfuni 4442 |
. . . . . . 7
|
10 | 9 | nfcsb1 3548 |
. . . . . 6
|
11 | 10 | nfeq1 2778 |
. . . . 5
|
12 | 2, 11 | nfral 2945 |
. . . 4
|
13 | | eqeq2 2633 |
. . . . 5
|
14 | 13 | raleqbi1dv 3146 |
. . . 4
|
15 | | vex 3203 |
. . . . 5
|
16 | 15 | a1i 11 |
. . . 4
Disj
|
17 | | simplll 798 |
. . . . . . . . . . . . 13
Disj
Disj |
18 | | simpllr 799 |
. . . . . . . . . . . . 13
Disj
|
19 | | simprl 794 |
. . . . . . . . . . . . 13
Disj
|
20 | | simplr 792 |
. . . . . . . . . . . . 13
Disj
|
21 | | simprr 796 |
. . . . . . . . . . . . 13
Disj
|
22 | | csbeq1a 3542 |
. . . . . . . . . . . . . 14
|
23 | 3, 5, 22 | disjif2 29394 |
. . . . . . . . . . . . 13
Disj
|
24 | 17, 18, 19, 20, 21, 23 | syl122anc 1335 |
. . . . . . . . . . . 12
Disj
|
25 | | simpr 477 |
. . . . . . . . . . . . . 14
Disj
|
26 | | simpllr 799 |
. . . . . . . . . . . . . 14
Disj
|
27 | 25, 26 | eqeltrrd 2702 |
. . . . . . . . . . . . 13
Disj
|
28 | | simplr 792 |
. . . . . . . . . . . . . 14
Disj
|
29 | 22 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
|
30 | 25, 29 | syl 17 |
. . . . . . . . . . . . . 14
Disj
|
31 | 28, 30 | mpbid 222 |
. . . . . . . . . . . . 13
Disj
|
32 | 27, 31 | jca 554 |
. . . . . . . . . . . 12
Disj
|
33 | 24, 32 | impbida 877 |
. . . . . . . . . . 11
Disj
|
34 | | equcom 1945 |
. . . . . . . . . . 11
|
35 | 33, 34 | syl6bb 276 |
. . . . . . . . . 10
Disj
|
36 | 35 | abbidv 2741 |
. . . . . . . . 9
Disj
|
37 | | df-sn 4178 |
. . . . . . . . 9
|
38 | 36, 37 | syl6eqr 2674 |
. . . . . . . 8
Disj
|
39 | 38 | unieqd 4446 |
. . . . . . 7
Disj
|
40 | | vex 3203 |
. . . . . . . 8
|
41 | 40 | unisn 4451 |
. . . . . . 7
|
42 | 39, 41 | syl6eq 2672 |
. . . . . 6
Disj
|
43 | | csbeq1 3536 |
. . . . . . 7
|
44 | | csbid 3541 |
. . . . . . 7
|
45 | 43, 44 | syl6eq 2672 |
. . . . . 6
|
46 | 42, 45 | syl 17 |
. . . . 5
Disj
|
47 | 46 | ralrimiva 2966 |
. . . 4
Disj
|
48 | 1, 12, 14, 16, 47 | elabreximd 29348 |
. . 3
Disj
|
49 | 48 | ralrimiva 2966 |
. 2
Disj
|
50 | | invdisj 4638 |
. 2
Disj
|
51 | 49, 50 | syl 17 |
1
Disj
Disj
|