Step | Hyp | Ref
| Expression |
1 | | fveq2 5879 |
. . . . . 6
   VDeg
      VDeg       |
2 | 1 | eqeq1d 2473 |
. . . . 5
    VDeg    
  VDeg        |
3 | 2 | cbvrabv 3030 |
. . . 4
   VDeg         VDeg       |
4 | | eqid 2471 |
. . . 4
    VDeg           VDeg        |
5 | 3, 4 | frgrawopreg 25856 |
. . 3
 FriendGrph      
  VDeg
         VDeg               VDeg            VDeg           |
6 | | fveq2 5879 |
. . . . . . . . . 10
   VDeg
      VDeg       |
7 | 6 | eqeq1d 2473 |
. . . . . . . . 9
    VDeg    
  VDeg        |
8 | 7 | cbvrabv 3030 |
. . . . . . . 8
   VDeg         VDeg       |
9 | | fveq2 5879 |
. . . . . . . . . . 11
   VDeg
      VDeg       |
10 | 9 | eqeq1d 2473 |
. . . . . . . . . 10
    VDeg    
  VDeg        |
11 | 10 | cbvrabv 3030 |
. . . . . . . . 9
   VDeg         VDeg       |
12 | 11 | difeq2i 3537 |
. . . . . . . 8
    VDeg           VDeg        |
13 | 8, 12 | frgrawopreg1 25857 |
. . . . . . 7
  FriendGrph
      VDeg       

           |
14 | 13 | 3mix3d 1207 |
. . . . . 6
  FriendGrph
      VDeg       
 
  VDeg
       VDeg      
       
   |
15 | 14 | expcom 442 |
. . . . 5
    
  VDeg
       FriendGrph     VDeg        VDeg     
             |
16 | | rabeq0 3757 |
. . . . . 6
    VDeg      
  VDeg       |
17 | | df-ne 2643 |
. . . . . . . . . 10
   VDeg    
  VDeg       |
18 | 17 | biimpri 211 |
. . . . . . . . 9
   VDeg    
  VDeg       |
19 | 18 | ralimi 2796 |
. . . . . . . 8
 
  VDeg    

  VDeg       |
20 | 19 | 3mix2d 1206 |
. . . . . . 7
 
  VDeg    
 
  VDeg
       VDeg      
       
   |
21 | 20 | a1d 25 |
. . . . . 6
 
  VDeg    
 FriendGrph  
  VDeg        VDeg     
             |
22 | 16, 21 | sylbi 200 |
. . . . 5
    VDeg       FriendGrph
    VDeg    

  VDeg      
       
    |
23 | 15, 22 | jaoi 386 |
. . . 4
        VDeg          VDeg        FriendGrph     VDeg        VDeg     
             |
24 | | fveq2 5879 |
. . . . . . . . . 10
   VDeg
      VDeg       |
25 | 24 | eqeq1d 2473 |
. . . . . . . . 9
    VDeg    
  VDeg        |
26 | 25 | cbvrabv 3030 |
. . . . . . . 8
   VDeg         VDeg       |
27 | 8 | difeq2i 3537 |
. . . . . . . 8
    VDeg           VDeg        |
28 | 26, 27 | frgrawopreg2 25858 |
. . . . . . 7
  FriendGrph
       VDeg        

           |
29 | 28 | 3mix3d 1207 |
. . . . . 6
  FriendGrph
       VDeg        
 
  VDeg
       VDeg      
       
   |
30 | 29 | expcom 442 |
. . . . 5
        VDeg         FriendGrph     VDeg        VDeg     
             |
31 | | difrab0eq 3828 |
. . . . . 6
     VDeg          VDeg        |
32 | | rabid2 2954 |
. . . . . . 7
    VDeg         VDeg       |
33 | | 3mix1 1199 |
. . . . . . . 8
 
  VDeg
     
  VDeg        VDeg     
            |
34 | 33 | a1d 25 |
. . . . . . 7
 
  VDeg
     FriendGrph     VDeg        VDeg     
             |
35 | 32, 34 | sylbi 200 |
. . . . . 6
    VDeg     
 FriendGrph  
  VDeg        VDeg     
             |
36 | 31, 35 | sylbi 200 |
. . . . 5
     VDeg        FriendGrph     VDeg        VDeg     
             |
37 | 30, 36 | jaoi 386 |
. . . 4
         VDeg            VDeg         FriendGrph     VDeg        VDeg     
             |
38 | 23, 37 | jaoi 386 |
. . 3
         VDeg          VDeg      
        VDeg            VDeg          FriendGrph     VDeg        VDeg     
             |
39 | 5, 38 | mpcom 36 |
. 2
 FriendGrph  
  VDeg        VDeg     
            |
40 | | biidd 245 |
. . 3
 FriendGrph  
  VDeg    

  VDeg        |
41 | | biidd 245 |
. . 3
 FriendGrph  
  VDeg    

  VDeg        |
42 | | sneq 3969 |
. . . . . . 7
       |
43 | 42 | difeq2d 3540 |
. . . . . 6
           |
44 | | preq1 4042 |
. . . . . . 7
         |
45 | 44 | eleq1d 2533 |
. . . . . 6
    
      |
46 | 43, 45 | raleqbidv 2987 |
. . . . 5
  
        
           |
47 | 46 | cbvrexv 3006 |
. . . 4
  
       

           |
48 | 47 | a1i 11 |
. . 3
 FriendGrph  
        

            |
49 | 40, 41, 48 | 3orbi123d 1364 |
. 2
 FriendGrph   
  VDeg
       VDeg      
       
     VDeg        VDeg     
             |
50 | 39, 49 | mpbird 240 |
1
 FriendGrph  
  VDeg        VDeg     
            |