Theorem bj-xpimasn

Description: The image of a singleton, general case. [Change and relabel xpimasn accordingly, maybe to xpima2sn.] (Contributed by BJ, 6-Apr-2019)

	Ref	Expression
Assertion	bj-xpimasn	⊢ ( ( 𝐴 × 𝐵 ) “ { 𝑋 } ) = if ( 𝑋 ∈ 𝐴 , 𝐵 , ∅ )

Proof

Step	Hyp	Ref	Expression
1		xpima	⊢ ( ( 𝐴 × 𝐵 ) “ { 𝑋 } ) = if ( ( 𝐴 ∩ { 𝑋 } ) = ∅ , ∅ , 𝐵 )
2		disjsn	⊢ ( ( 𝐴 ∩ { 𝑋 } ) = ∅ ↔ ¬ 𝑋 ∈ 𝐴 )
3		eqid	⊢ 𝐵 = 𝐵
4	2 3	ifbieq2i	⊢ if ( ( 𝐴 ∩ { 𝑋 } ) = ∅ , ∅ , 𝐵 ) = if ( ¬ 𝑋 ∈ 𝐴 , ∅ , 𝐵 )
5		ifnot	⊢ if ( ¬ 𝑋 ∈ 𝐴 , ∅ , 𝐵 ) = if ( 𝑋 ∈ 𝐴 , 𝐵 , ∅ )
6	1 4 5	3eqtri	⊢ ( ( 𝐴 × 𝐵 ) “ { 𝑋 } ) = if ( 𝑋 ∈ 𝐴 , 𝐵 , ∅ )