Step | Hyp | Ref
| Expression |
1 | | excom 1927 |
. . . . . 6
                     |
2 | | nfv 1761 |
. . . . . . . . . . 11

    |
3 | | cnvoprab.x |
. . . . . . . . . . 11
   |
4 | 2, 3 | nfan 2011 |
. . . . . . . . . 10
        |
5 | 4 | nfex 2031 |
. . . . . . . . 9
          |
6 | | nfv 1761 |
. . . . . . . . . . . 12
     |
7 | | cnvoprab.y |
. . . . . . . . . . . 12
   |
8 | 6, 7 | nfan 2011 |
. . . . . . . . . . 11
        |
9 | 8 | nfex 2031 |
. . . . . . . . . 10
          |
10 | | opex 4664 |
. . . . . . . . . . 11
    |
11 | | opeq1 4166 |
. . . . . . . . . . . . 13
      
        |
12 | 11 | eqeq2d 2461 |
. . . . . . . . . . . 12
            
    |
13 | | cnvoprab.1 |
. . . . . . . . . . . 12
    
   |
14 | 12, 13 | anbi12d 717 |
. . . . . . . . . . 11
         
     
     |
15 | 10, 14 | spcev 3141 |
. . . . . . . . . 10
                  |
16 | 9, 15 | exlimi 1995 |
. . . . . . . . 9
        
           |
17 | 5, 16 | exlimi 1995 |
. . . . . . . 8
                      |
18 | | cnvoprab.2 |
. . . . . . . . . . 11

    |
19 | 18 | adantl 468 |
. . . . . . . . . 10
          |
20 | | fvex 5875 |
. . . . . . . . . . 11
     |
21 | | fvex 5875 |
. . . . . . . . . . 11
     |
22 | | eqcom 2458 |
. . . . . . . . . . . . . . 15
    
      |
23 | | eqcom 2458 |
. . . . . . . . . . . . . . 15
    
      |
24 | 22, 23 | anbi12i 703 |
. . . . . . . . . . . . . 14
          
    
       |
25 | | eqopi 6827 |
. . . . . . . . . . . . . 14
                    |
26 | 24, 25 | sylan2br 479 |
. . . . . . . . . . . . 13
                    |
27 | 14 | bicomd 205 |
. . . . . . . . . . . . 13
          
 
        |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
                     
 
        |
29 | 4, 8, 28 | spc2ed 28106 |
. . . . . . . . . . 11
                                    |
30 | 20, 21, 29 | mpanr12 691 |
. . . . . . . . . 10
  
                     |
31 | 19, 30 | mpcom 37 |
. . . . . . . . 9
                    |
32 | 31 | exlimiv 1776 |
. . . . . . . 8
                 
    |
33 | 17, 32 | impbii 191 |
. . . . . . 7
            
         |
34 | 33 | exbii 1718 |
. . . . . 6
            
 
           |
35 | | exrot3 1931 |
. . . . . 6
            
 
                |
36 | 1, 34, 35 | 3bitr2ri 278 |
. . . . 5
            
 
           |
37 | 36 | abbii 2567 |
. . . 4
            
   
           |
38 | | df-oprab 6294 |
. . . 4
       
            
    |
39 | | df-opab 4462 |
. . . 4
    
            |
40 | 37, 38, 39 | 3eqtr4ri 2484 |
. . 3
    
      
  |
41 | 40 | cnveqi 5009 |
. 2
            
   |
42 | | cnvopab 5237 |
. 2
            |
43 | 41, 42 | eqtr3i 2475 |
1
      
        |