Step | Hyp | Ref
| Expression |
1 | | elex 3087 |
. 2
  Image
Singleton   
  |
2 | | ssnid 4015 |
. . . . 5
   |
3 | | eleq2 2527 |
. . . . 5
               
     |
4 | 2, 3 | mpbiri 233 |
. . . 4
                 |
5 | | n0i 3751 |
. . . . 5
               |
6 | | snprc 4048 |
. . . . . . . 8

 
  |
7 | 6 | biimpi 194 |
. . . . . . 7
     |
8 | 7 | imaeq2d 5278 |
. . . . . 6
             |
9 | | ima0 5293 |
. . . . . 6
     |
10 | 8, 9 | syl6eq 2511 |
. . . . 5
         |
11 | 5, 10 | nsyl2 127 |
. . . 4
      
  |
12 | 4, 11 | syl 16 |
. . 3
           |
13 | 12 | exlimiv 1689 |
. 2
             |
14 | | eleq1 2526 |
. . 3
   Image
Singleton   
 Image Singleton       |
15 | | sneq 3996 |
. . . . . 6
       |
16 | 15 | imaeq2d 5278 |
. . . . 5
               |
17 | 16 | eqeq1d 2456 |
. . . 4
         
           |
18 | 17 | exbidv 1681 |
. . 3
                         |
19 | | vex 3081 |
. . . . 5
 |
20 | 19 | eldm 5146 |
. . . 4
  Image
Singleton   
   Image Singleton       |
21 | | brxp 4979 |
. . . . . . . . . 10
    
    |
22 | 19, 21 | mpbiran 909 |
. . . . . . . . 9
    
  |
23 | | elsingles 28094 |
. . . . . . . . 9
      |
24 | 22, 23 | bitri 249 |
. . . . . . . 8
    

    |
25 | 24 | anbi2i 694 |
. . . . . . 7
   Image Singleton        Image Singleton 
     |
26 | | brin 4450 |
. . . . . . 7
   Image Singleton    
  Image
Singleton        |
27 | | 19.42v 1936 |
. . . . . . 7
     Image
Singleton
  
  Image
Singleton       |
28 | 25, 26, 27 | 3bitr4i 277 |
. . . . . 6
   Image Singleton    
    Image Singleton      |
29 | 28 | exbii 1635 |
. . . . 5
    Image
Singleton           Image Singleton      |
30 | | excom 1789 |
. . . . 5
       Image Singleton          Image Singleton      |
31 | 29, 30 | bitri 249 |
. . . 4
    Image
Singleton           Image Singleton      |
32 | | exancom 1639 |
. . . . . 6
     Image
Singleton
  
      Image
Singleton    |
33 | | snex 4642 |
. . . . . . 7
 
 |
34 | | breq2 4405 |
. . . . . . 7
     Image Singleton
 Image
Singleton      |
35 | 33, 34 | ceqsexv 3115 |
. . . . . 6
       Image Singleton   Image Singleton     |
36 | 19, 33 | brco 5119 |
. . . . . . 7
  Image Singleton  
   Singleton Image      |
37 | | vex 3081 |
. . . . . . . . . 10
 |
38 | 19, 37 | brsingle 28093 |
. . . . . . . . 9
 Singleton     |
39 | 38 | anbi1i 695 |
. . . . . . . 8
  Singleton Image       Image      |
40 | 39 | exbii 1635 |
. . . . . . 7
    Singleton Image   
     Image      |
41 | | snex 4642 |
. . . . . . . . 9
   |
42 | | breq1 4404 |
. . . . . . . . 9
    Image  
  Image      |
43 | 41, 42 | ceqsexv 3115 |
. . . . . . . 8
      Image      Image     |
44 | 41, 33 | brimage 28102 |
. . . . . . . 8
   Image  
 
        |
45 | | eqcom 2463 |
. . . . . . . 8
        
          |
46 | 43, 44, 45 | 3bitri 271 |
. . . . . . 7
      Image              |
47 | 36, 40, 46 | 3bitri 271 |
. . . . . 6
  Image Singleton  
          |
48 | 32, 35, 47 | 3bitri 271 |
. . . . 5
     Image
Singleton
  
          |
49 | 48 | exbii 1635 |
. . . 4
       Image Singleton                |
50 | 20, 31, 49 | 3bitri 271 |
. . 3
  Image
Singleton   
            |
51 | 14, 18, 50 | vtoclbg 3137 |
. 2
 
 Image
Singleton   
             |
52 | 1, 13, 51 | pm5.21nii 353 |
1
  Image
Singleton   
            |