Theorem bj-xpima2sn

Description: The image of a singleton by a direct product, nonempty case. [To replace xpimasn .] (Contributed by BJ, 6-Apr-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-xpima2sn	|- ( X e. A -> ( ( A X. B ) " { X } ) = B )

Proof

Step	Hyp	Ref	Expression
1		bj-xpimasn	|- ( ( A X. B ) " { X } ) = if ( X e. A , B , (/) )
2		iftrue	|- ( X e. A -> if ( X e. A , B , (/) ) = B )
3	1 2	syl5eq	|- ( X e. A -> ( ( A X. B ) " { X } ) = B )