Step | Hyp | Ref
| Expression |
1 | | nfdisj1 4385 |
. . . 4
 Disj  |
2 | | nfcv 2591 |
. . . . 5
   |
3 | | nfv 1760 |
. . . . . . . . . 10

 |
4 | | nfcsb1v 3378 |
. . . . . . . . . . 11
  
 ![]_ ]_](_urbrack.gif)  |
5 | 4 | nfcri 2585 |
. . . . . . . . . 10

  ![]_ ]_](_urbrack.gif)  |
6 | 3, 5 | nfan 2010 |
. . . . . . . . 9
  
  ![]_ ]_](_urbrack.gif)   |
7 | 6 | nfab 2595 |
. . . . . . . 8
   
  ![]_ ]_](_urbrack.gif)    |
8 | 7 | nfuni 4203 |
. . . . . . 7
    
  ![]_ ]_](_urbrack.gif)    |
9 | 8 | nfcsb1 3377 |
. . . . . 6
     
  ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)  |
10 | 9 | nfeq1 2604 |
. . . . 5
     
  ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)
 |
11 | 2, 10 | nfral 2773 |
. . . 4
  
   
  ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)
 |
12 | | eqeq2 2461 |
. . . . 5
     
  ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
13 | 12 | raleqbi1dv 2994 |
. . . 4
  
   
  ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)

      ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)    |
14 | | vex 3047 |
. . . . 5
 |
15 | 14 | a1i 11 |
. . . 4
Disj
  |
16 | | simplll 767 |
. . . . . . . . . . . . 13
   Disj
  
  ![]_ ]_](_urbrack.gif)   Disj   |
17 | | simpllr 768 |
. . . . . . . . . . . . 13
   Disj
  
  ![]_ ]_](_urbrack.gif)     |
18 | | simprl 763 |
. . . . . . . . . . . . 13
   Disj
  
  ![]_ ]_](_urbrack.gif)     |
19 | | simplr 761 |
. . . . . . . . . . . . 13
   Disj
  
  ![]_ ]_](_urbrack.gif)     |
20 | | simprr 765 |
. . . . . . . . . . . . 13
   Disj
  
  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
21 | | csbeq1a 3371 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)   |
22 | 4, 21 | disjif 28181 |
. . . . . . . . . . . . 13
 Disj



  ![]_ ]_](_urbrack.gif)  
  |
23 | 16, 17, 18, 19, 20, 22 | syl122anc 1276 |
. . . . . . . . . . . 12
   Disj
  
  ![]_ ]_](_urbrack.gif)     |
24 | | simpr 463 |
. . . . . . . . . . . . . 14
   Disj
  
  |
25 | | simpllr 768 |
. . . . . . . . . . . . . 14
   Disj
  
  |
26 | 24, 25 | eqeltrrd 2529 |
. . . . . . . . . . . . 13
   Disj
     |
27 | | simplr 761 |
. . . . . . . . . . . . . 14
   Disj
     |
28 | 21 | eleq2d 2513 |
. . . . . . . . . . . . . . 15
 
  ![]_ ]_](_urbrack.gif)    |
29 | 24, 28 | syl 17 |
. . . . . . . . . . . . . 14
   Disj
      ![]_ ]_](_urbrack.gif)    |
30 | 27, 29 | mpbid 214 |
. . . . . . . . . . . . 13
   Disj
     ![]_ ]_](_urbrack.gif)   |
31 | 26, 30 | jca 535 |
. . . . . . . . . . . 12
   Disj
   
  ![]_ ]_](_urbrack.gif)    |
32 | 23, 31 | impbida 842 |
. . . . . . . . . . 11
  Disj

  
  ![]_ ]_](_urbrack.gif)     |
33 | | equcom 1861 |
. . . . . . . . . . 11

  |
34 | 32, 33 | syl6bb 265 |
. . . . . . . . . 10
  Disj

  
  ![]_ ]_](_urbrack.gif)     |
35 | 34 | abbidv 2568 |
. . . . . . . . 9
  Disj

     ![]_ ]_](_urbrack.gif)       |
36 | | df-sn 3968 |
. . . . . . . . 9
 

  |
37 | 35, 36 | syl6eqr 2502 |
. . . . . . . 8
  Disj

     ![]_ ]_](_urbrack.gif)       |
38 | 37 | unieqd 4207 |
. . . . . . 7
  Disj

      ![]_ ]_](_urbrack.gif)        |
39 | | vex 3047 |
. . . . . . . 8
 |
40 | 39 | unisn 4212 |
. . . . . . 7
    |
41 | 38, 40 | syl6eq 2500 |
. . . . . 6
  Disj

      ![]_ ]_](_urbrack.gif)     |
42 | | csbeq1 3365 |
. . . . . . 7
   
  ![]_ ]_](_urbrack.gif)      
  ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
43 | | csbid 3370 |
. . . . . . 7
  ![]_ ]_](_urbrack.gif)  |
44 | 42, 43 | syl6eq 2500 |
. . . . . 6
   
  ![]_ ]_](_urbrack.gif)      
  ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
45 | 41, 44 | syl 17 |
. . . . 5
  Disj

    
  ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
46 | 45 | ralrimiva 2801 |
. . . 4
 Disj


      ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
47 | 1, 11, 13, 15, 46 | elabreximd 28137 |
. . 3
 Disj
    
      ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
48 | 47 | ralrimiva 2801 |
. 2
Disj
            ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)   |
49 | | invdisj 4390 |
. 2
 
 
  
   
  ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)
Disj  
    |
50 | 48, 49 | syl 17 |
1
Disj
Disj  
    |