Metamath Proof Explorer


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 A × B X = if X A B

Proof

Step Hyp Ref Expression
1 xpima A × B X = if A X = B
2 disjsn A X = ¬ X A
3 eqid B = B
4 2 3 ifbieq2i if A X = B = if ¬ X A B
5 ifnot if ¬ X A B = if X A B
6 1 4 5 3eqtri A × B X = if X A B