Step | Hyp | Ref
| Expression |
1 | | elex 3212 |
. 2
  Image
Singleton   
  |
2 | | vsnid 4209 |
. . . . 5
   |
3 | | eleq2 2690 |
. . . . 5
               
     |
4 | 2, 3 | mpbiri 248 |
. . . 4
                 |
5 | | n0i 3920 |
. . . . 5
               |
6 | | snprc 4253 |
. . . . . . . 8

 
  |
7 | 6 | biimpi 206 |
. . . . . . 7
     |
8 | 7 | imaeq2d 5466 |
. . . . . 6
             |
9 | | ima0 5481 |
. . . . . 6
     |
10 | 8, 9 | syl6eq 2672 |
. . . . 5
         |
11 | 5, 10 | nsyl2 142 |
. . . 4
      
  |
12 | 4, 11 | syl 17 |
. . 3
           |
13 | 12 | exlimiv 1858 |
. 2
             |
14 | | eleq1 2689 |
. . 3
   Image
Singleton   
 Image Singleton       |
15 | | sneq 4187 |
. . . . . 6
       |
16 | 15 | imaeq2d 5466 |
. . . . 5
               |
17 | 16 | eqeq1d 2624 |
. . . 4
         
           |
18 | 17 | exbidv 1850 |
. . 3
                         |
19 | | vex 3203 |
. . . . 5
 |
20 | 19 | eldm 5321 |
. . . 4
  Image
Singleton   
   Image Singleton       |
21 | | brxp 5147 |
. . . . . . . . . 10
    
    |
22 | 19, 21 | mpbiran 953 |
. . . . . . . . 9
    
  |
23 | | elsingles 32025 |
. . . . . . . . 9
      |
24 | 22, 23 | bitri 264 |
. . . . . . . 8
    

    |
25 | 24 | anbi2i 730 |
. . . . . . 7
   Image Singleton        Image Singleton 
     |
26 | | brin 4704 |
. . . . . . 7
   Image Singleton    
  Image
Singleton        |
27 | | 19.42v 1918 |
. . . . . . 7
     Image
Singleton
  
  Image
Singleton       |
28 | 25, 26, 27 | 3bitr4i 292 |
. . . . . 6
   Image Singleton    
    Image Singleton      |
29 | 28 | exbii 1774 |
. . . . 5
    Image
Singleton           Image Singleton      |
30 | | excom 2042 |
. . . . 5
       Image Singleton          Image Singleton      |
31 | 29, 30 | bitri 264 |
. . . 4
    Image
Singleton           Image Singleton      |
32 | | exancom 1787 |
. . . . . 6
     Image
Singleton
  
      Image
Singleton    |
33 | | snex 4908 |
. . . . . . 7
 
 |
34 | | breq2 4657 |
. . . . . . 7
     Image Singleton
 Image
Singleton      |
35 | 33, 34 | ceqsexv 3242 |
. . . . . 6
       Image Singleton   Image Singleton     |
36 | 19, 33 | brco 5292 |
. . . . . . 7
  Image Singleton  
   Singleton Image      |
37 | | vex 3203 |
. . . . . . . . . 10
 |
38 | 19, 37 | brsingle 32024 |
. . . . . . . . 9
 Singleton     |
39 | 38 | anbi1i 731 |
. . . . . . . 8
  Singleton Image       Image      |
40 | 39 | exbii 1774 |
. . . . . . 7
    Singleton Image   
     Image      |
41 | | snex 4908 |
. . . . . . . . 9
   |
42 | | breq1 4656 |
. . . . . . . . 9
    Image  
  Image      |
43 | 41, 42 | ceqsexv 3242 |
. . . . . . . 8
      Image      Image     |
44 | 41, 33 | brimage 32033 |
. . . . . . . 8
   Image  
 
        |
45 | | eqcom 2629 |
. . . . . . . 8
        
          |
46 | 43, 44, 45 | 3bitri 286 |
. . . . . . 7
      Image              |
47 | 36, 40, 46 | 3bitri 286 |
. . . . . 6
  Image Singleton  
          |
48 | 32, 35, 47 | 3bitri 286 |
. . . . 5
     Image
Singleton
  
          |
49 | 48 | exbii 1774 |
. . . 4
       Image Singleton                |
50 | 20, 31, 49 | 3bitri 286 |
. . 3
  Image
Singleton   
            |
51 | 14, 18, 50 | vtoclbg 3267 |
. 2
 
 Image
Singleton   
             |
52 | 1, 13, 51 | pm5.21nii 368 |
1
  Image
Singleton   
            |