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	⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝐴 × 𝐵 ) “ { 𝑋 } ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		bj-xpimasn	⊢ ( ( 𝐴 × 𝐵 ) “ { 𝑋 } ) = if ( 𝑋 ∈ 𝐴 , 𝐵 , ∅ )
2		iftrue	⊢ ( 𝑋 ∈ 𝐴 → if ( 𝑋 ∈ 𝐴 , 𝐵 , ∅ ) = 𝐵 )
3	1 2	syl5eq	⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝐴 × 𝐵 ) “ { 𝑋 } ) = 𝐵 )