Metamath Proof Explorer

Theorem ex-opab

Description: Example for df-opab . Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Assertion ex-opab 
|- ( R = { <. x , y >. | ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) } -> 3 R 4 )

Proof

Step Hyp Ref Expression
1 3cn 
 |-  3 e. CC
2 4cn 
 |-  4 e. CC
3 3p1e4 
 |-  ( 3 + 1 ) = 4
4 1 elexi 
 |-  3 e. _V
5 2 elexi 
 |-  4 e. _V
6 eleq1 
 |-  ( x = 3 -> ( x e. CC <-> 3 e. CC ) )
7 oveq1 
 |-  ( x = 3 -> ( x + 1 ) = ( 3 + 1 ) )
8 7 eqeq1d 
 |-  ( x = 3 -> ( ( x + 1 ) = y <-> ( 3 + 1 ) = y ) )
9 6 8 3anbi13d 
 |-  ( x = 3 -> ( ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) <-> ( 3 e. CC /\ y e. CC /\ ( 3 + 1 ) = y ) ) )
10 eleq1 
 |-  ( y = 4 -> ( y e. CC <-> 4 e. CC ) )
11 eqeq2 
 |-  ( y = 4 -> ( ( 3 + 1 ) = y <-> ( 3 + 1 ) = 4 ) )
12 10 11 3anbi23d 
 |-  ( y = 4 -> ( ( 3 e. CC /\ y e. CC /\ ( 3 + 1 ) = y ) <-> ( 3 e. CC /\ 4 e. CC /\ ( 3 + 1 ) = 4 ) ) )
13 eqid 
 |-  { <. x , y >. | ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) } = { <. x , y >. | ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) }
14 4 5 9 12 13 brab 
 |-  ( 3 { <. x , y >. | ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) } 4 <-> ( 3 e. CC /\ 4 e. CC /\ ( 3 + 1 ) = 4 ) )
15 1 2 3 14 mpbir3an 
 |-  3 { <. x , y >. | ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) } 4
16 breq 
 |-  ( R = { <. x , y >. | ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) } -> ( 3 R 4 <-> 3 { <. x , y >. | ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) } 4 ) )
17 15 16 mpbiri 
 |-  ( R = { <. x , y >. | ( x e. CC /\ y e. CC /\ ( x + 1 ) = y ) } -> 3 R 4 )