Metamath Proof Explorer

Theorem bj-xpnzexb

Description: If the first factor of a product is a nonempty set, then the product is a set if and only if the second factor is a set. (Contributed by BJ, 2-Apr-2019)

		Ref	Expression
	Assertion	bj-xpnzexb	$⊢ A \in (V ∖ \{\emptyset\}) \to (B \in V \leftrightarrow A \times B \in V)$

Proof

Step	Hyp	Ref	Expression
1		bj-xpexg2	$⊢ A \in (V ∖ \{\emptyset\}) \to (B \in V \to A \times B \in V)$
2		eldifsni	$⊢ A \in (V ∖ \{\emptyset\}) \to A \neq \emptyset$
3		bj-xpnzex	$⊢ A \neq \emptyset \to (A \times B \in V \to B \in V)$
4	2 3	syl	$⊢ A \in (V ∖ \{\emptyset\}) \to (A \times B \in V \to B \in V)$
5	1 4	impbid	$⊢ A \in (V ∖ \{\emptyset\}) \to (B \in V \leftrightarrow A \times B \in V)$