This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xpima2

Description: Direct image by a Cartesian product (case of nonempty intersection with the domain). (Contributed by Thierry Arnoux, 16-Dec-2017)

		Ref	Expression
	Assertion	xpima2	$⊢ A \cap C \neq \emptyset \to (A \times B) [C] = B$

Step	Hyp	Ref	Expression
1		xpima	$⊢ (A \times B) [C] = if (A \cap C = \emptyset, \emptyset, B)$
2		ifnefalse	$⊢ A \cap C \neq \emptyset \to if (A \cap C = \emptyset, \emptyset, B) = B$
3	1 2	eqtrid	$⊢ A \cap C \neq \emptyset \to (A \times B) [C] = B$