Theorem fvdiagfn

Description: Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypothesis	fdiagfn.f	|- F = ( x e. B |-> ( I X. { x } ) )
Assertion	fvdiagfn	|- ( ( I e. W /\ X e. B ) -> ( F ` X ) = ( I X. { X } ) )

Proof

Step	Hyp	Ref	Expression
1		fdiagfn.f	|- F = ( x e. B |-> ( I X. { x } ) )
2		sneq	|- ( x = X -> { x } = { X } )
3	2	xpeq2d	|- ( x = X -> ( I X. { x } ) = ( I X. { X } ) )
4		simpr	|- ( ( I e. W /\ X e. B ) -> X e. B )
5		snex	|- { X } e. _V
6		xpexg	|- ( ( I e. W /\ { X } e. _V ) -> ( I X. { X } ) e. _V )
7	5 6	mpan2	|- ( I e. W -> ( I X. { X } ) e. _V )
8	7	adantr	|- ( ( I e. W /\ X e. B ) -> ( I X. { X } ) e. _V )
9	1 3 4 8	fvmptd3	|- ( ( I e. W /\ X e. B ) -> ( F ` X ) = ( I X. { X } ) )