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 ) } )