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

Metamath Proof Explorer

Theorem xpexcnv

Description: A condition where the converse of xpex holds as well. Corollary 6.9(2) in TakeutiZaring p. 26. (Contributed by Andrew Salmon, 13-Nov-2011)

		Ref	Expression
	Assertion	xpexcnv	$⊢ (B \neq \emptyset \land A \times B \in V) \to A \in V$

Proof

Step	Hyp	Ref	Expression
1		dmexg	$⊢ A \times B \in V \to dom (A \times B) \in V$
2		dmxp	$⊢ B \neq \emptyset \to dom (A \times B) = A$
3	2	eleq1d	$⊢ B \neq \emptyset \to (dom (A \times B) \in V \leftrightarrow A \in V)$
4	1 3	imbitrid	$⊢ B \neq \emptyset \to (A \times B \in V \to A \in V)$
5	4	imp	$⊢ (B \neq \emptyset \land A \times B \in V) \to A \in V$