This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ixpsnval

Description: The value of an infinite Cartesian product with a singleton. (Contributed by AV, 3-Dec-2018)

Ref Expression
Assertion ixpsnval 
|- ( X e. V -> X_ x e. { X } B = { f | ( f Fn { X } /\ ( f ` X ) e. [_ X / x ]_ B ) } )

Proof

Step Hyp Ref Expression
1 dfixp 
 |-  X_ x e. { X } B = { f | ( f Fn { X } /\ A. x e. { X } ( f ` x ) e. B ) }
2 ralsnsg 
 |-  ( X e. V -> ( A. x e. { X } ( f ` x ) e. B <-> [. X / x ]. ( f ` x ) e. B ) )
3 sbcel12 
 |-  ( [. X / x ]. ( f ` x ) e. B <-> [_ X / x ]_ ( f ` x ) e. [_ X / x ]_ B )
4 csbfv2g 
 |-  ( X e. V -> [_ X / x ]_ ( f ` x ) = ( f ` [_ X / x ]_ x ) )
5 csbvarg 
 |-  ( X e. V -> [_ X / x ]_ x = X )
6 5 fveq2d 
 |-  ( X e. V -> ( f ` [_ X / x ]_ x ) = ( f ` X ) )
7 4 6 eqtrd 
 |-  ( X e. V -> [_ X / x ]_ ( f ` x ) = ( f ` X ) )
8 7 eleq1d 
 |-  ( X e. V -> ( [_ X / x ]_ ( f ` x ) e. [_ X / x ]_ B <-> ( f ` X ) e. [_ X / x ]_ B ) )
9 3 8 bitrid 
 |-  ( X e. V -> ( [. X / x ]. ( f ` x ) e. B <-> ( f ` X ) e. [_ X / x ]_ B ) )
10 2 9 bitrd 
 |-  ( X e. V -> ( A. x e. { X } ( f ` x ) e. B <-> ( f ` X ) e. [_ X / x ]_ B ) )
11 10 anbi2d 
 |-  ( X e. V -> ( ( f Fn { X } /\ A. x e. { X } ( f ` x ) e. B ) <-> ( f Fn { X } /\ ( f ` X ) e. [_ X / x ]_ B ) ) )
12 11 abbidv 
 |-  ( X e. V -> { f | ( f Fn { X } /\ A. x e. { X } ( f ` x ) e. B ) } = { f | ( f Fn { X } /\ ( f ` X ) e. [_ X / x ]_ B ) } )
13 1 12 eqtrid 
 |-  ( X e. V -> X_ x e. { X } B = { f | ( f Fn { X } /\ ( f ` X ) e. [_ X / x ]_ B ) } )