Metamath Proof Explorer

Theorem fzprval

Description: Two ways of defining the first two values of a sequence on NN . (Contributed by NM, 5-Sep-2011)

Ref Expression
Assertion fzprval 
|- ( A. x e. ( 1 ... 2 ) ( F ` x ) = if ( x = 1 , A , B ) <-> ( ( F ` 1 ) = A /\ ( F ` 2 ) = B ) )

Proof

Step Hyp Ref Expression
1 fz12pr 
 |-  ( 1 ... 2 ) = { 1 , 2 }
2 1 raleqi 
 |-  ( A. x e. ( 1 ... 2 ) ( F ` x ) = if ( x = 1 , A , B ) <-> A. x e. { 1 , 2 } ( F ` x ) = if ( x = 1 , A , B ) )
3 1ex 
 |-  1 e. _V
4 2ex 
 |-  2 e. _V
5 fveq2 
 |-  ( x = 1 -> ( F ` x ) = ( F ` 1 ) )
6 iftrue 
 |-  ( x = 1 -> if ( x = 1 , A , B ) = A )
7 5 6 eqeq12d 
 |-  ( x = 1 -> ( ( F ` x ) = if ( x = 1 , A , B ) <-> ( F ` 1 ) = A ) )
8 fveq2 
 |-  ( x = 2 -> ( F ` x ) = ( F ` 2 ) )
9 1ne2 
 |-  1 =/= 2
10 9 necomi 
 |-  2 =/= 1
11 pm13.181 
 |-  ( ( x = 2 /\ 2 =/= 1 ) -> x =/= 1 )
12 10 11 mpan2 
 |-  ( x = 2 -> x =/= 1 )
13 12 neneqd 
 |-  ( x = 2 -> -. x = 1 )
14 13 iffalsed 
 |-  ( x = 2 -> if ( x = 1 , A , B ) = B )
15 8 14 eqeq12d 
 |-  ( x = 2 -> ( ( F ` x ) = if ( x = 1 , A , B ) <-> ( F ` 2 ) = B ) )
16 3 4 7 15 ralpr 
 |-  ( A. x e. { 1 , 2 } ( F ` x ) = if ( x = 1 , A , B ) <-> ( ( F ` 1 ) = A /\ ( F ` 2 ) = B ) )
17 2 16 bitri 
 |-  ( A. x e. ( 1 ... 2 ) ( F ` x ) = if ( x = 1 , A , B ) <-> ( ( F ` 1 ) = A /\ ( F ` 2 ) = B ) )