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	⊢ ( 𝐴 ∈ ( 𝑉 ∖ { ∅ } ) → ( 𝐵 ∈ V ↔ ( 𝐴 × 𝐵 ) ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		bj-xpexg2	⊢ ( 𝐴 ∈ ( 𝑉 ∖ { ∅ } ) → ( 𝐵 ∈ V → ( 𝐴 × 𝐵 ) ∈ V ) )
2		eldifsni	⊢ ( 𝐴 ∈ ( 𝑉 ∖ { ∅ } ) → 𝐴 ≠ ∅ )
3		bj-xpnzex	⊢ ( 𝐴 ≠ ∅ → ( ( 𝐴 × 𝐵 ) ∈ V → 𝐵 ∈ V ) )
4	2 3	syl	⊢ ( 𝐴 ∈ ( 𝑉 ∖ { ∅ } ) → ( ( 𝐴 × 𝐵 ) ∈ V → 𝐵 ∈ V ) )
5	1 4	impbid	⊢ ( 𝐴 ∈ ( 𝑉 ∖ { ∅ } ) → ( 𝐵 ∈ V ↔ ( 𝐴 × 𝐵 ) ∈ V ) )