Proof of Theorem ov3
Step | Hyp | Ref
| Expression |
1 | | ov3.1 |
. . 3
 |
2 | 1 | isseti 3050 |
. 2
  |
3 | | nfv 1760 |
. . 3
     
   |
4 | | nfcv 2591 |
. . . . 5
      |
5 | | ov3.3 |
. . . . . 6
     
    

                  
    |
6 | | nfoprab3 6339 |
. . . . . 6
       
    

                  
    |
7 | 5, 6 | nfcxfr 2589 |
. . . . 5
   |
8 | | nfcv 2591 |
. . . . 5
      |
9 | 4, 7, 8 | nfov 6314 |
. . . 4
             |
10 | 9 | nfeq1 2604 |
. . 3
             |
11 | | ov3.2 |
. . . . . . 7
      
  |
12 | 11 | eqeq2d 2460 |
. . . . . 6
           |
13 | 12 | copsex4g 4689 |
. . . . 5
  


                         
    |
14 | | opelxpi 4865 |
. . . . . 6
 
        |
15 | | opelxpi 4865 |
. . . . . 6
 
        |
16 | | nfcv 2591 |
. . . . . . 7
      |
17 | | nfcv 2591 |
. . . . . . 7
      |
18 | | nfcv 2591 |
. . . . . . 7
      |
19 | | nfv 1760 |
. . . . . . . 8
                     
  |
20 | | nfoprab1 6337 |
. . . . . . . . . . 11
       
    

                  
    |
21 | 5, 20 | nfcxfr 2589 |
. . . . . . . . . 10
   |
22 | | nfcv 2591 |
. . . . . . . . . 10
   |
23 | 16, 21, 22 | nfov 6314 |
. . . . . . . . 9
          |
24 | 23 | nfeq1 2604 |
. . . . . . . 8
          |
25 | 19, 24 | nfim 2002 |
. . . . . . 7
                      
          |
26 | | nfv 1760 |
. . . . . . . 8
                        
  |
27 | | nfoprab2 6338 |
. . . . . . . . . . 11
       
    

                  
    |
28 | 5, 27 | nfcxfr 2589 |
. . . . . . . . . 10
   |
29 | 17, 28, 18 | nfov 6314 |
. . . . . . . . 9
             |
30 | 29 | nfeq1 2604 |
. . . . . . . 8
             |
31 | 26, 30 | nfim 2002 |
. . . . . . 7
                         

            |
32 | | eqeq1 2454 |
. . . . . . . . . . 11
         
       |
33 | 32 | anbi1d 710 |
. . . . . . . . . 10
                   
       |
34 | 33 | anbi1d 710 |
. . . . . . . . 9
             

       
   
    |
35 | 34 | 4exbidv 1771 |
. . . . . . . 8
                     
                    
    |
36 | | oveq1 6295 |
. . . . . . . . 9
                 |
37 | 36 | eqeq1d 2452 |
. . . . . . . 8
                   |
38 | 35, 37 | imbi12d 322 |
. . . . . . 7
                      
     
            
   
   

           |
39 | | eqeq1 2454 |
. . . . . . . . . . 11
         
       |
40 | 39 | anbi2d 709 |
. . . . . . . . . 10
       
   
                     |
41 | 40 | anbi1d 710 |
. . . . . . . . 9
            
   
    
          
    |
42 | 41 | 4exbidv 1771 |
. . . . . . . 8
                
   
   
                       
    |
43 | | oveq2 6296 |
. . . . . . . . 9
                       |
44 | 43 | eqeq1d 2452 |
. . . . . . . 8
       
                 |
45 | 42, 44 | imbi12d 322 |
. . . . . . 7
                         

                               

              |
46 | | moeq 3213 |
. . . . . . . . . . . 12
  |
47 | 46 | mosubop 4699 |
. . . . . . . . . . 11
            |
48 | 47 | mosubop 4699 |
. . . . . . . . . 10
                     |
49 | | anass 654 |
. . . . . . . . . . . . . 14
         

       
    |
50 | 49 | 2exbii 1718 |
. . . . . . . . . . . . 13
             

                |
51 | | 19.42vv 1835 |
. . . . . . . . . . . . 13
              
           
    |
52 | 50, 51 | bitri 253 |
. . . . . . . . . . . 12
             

           
    |
53 | 52 | 2exbii 1718 |
. . . . . . . . . . 11
                 

                    |
54 | 53 | mobii 2321 |
. . . . . . . . . 10
               
   
                       |
55 | 48, 54 | mpbir 213 |
. . . . . . . . 9
                  
  |
56 | 55 | a1i 11 |
. . . . . . . 8
   
                 
   
   |
57 | 56, 5 | ovidi 6412 |
. . . . . . 7
   
                
   

       |
58 | 16, 17, 18, 25, 31, 38, 45, 57 | vtocl2gaf 3113 |
. . . . . 6
      
                  
          
              |
59 | 14, 15, 58 | syl2an 480 |
. . . . 5
  


                         

             |
60 | 13, 59 | sylbird 239 |
. . . 4
  


                |
61 | | eqeq2 2461 |
. . . 4
           
             |
62 | 60, 61 | mpbidi 220 |
. . 3
  


                |
63 | 3, 10, 62 | exlimd 1996 |
. 2
  


                 |
64 | 2, 63 | mpi 20 |
1
  


              |