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 e. ( V \ { (/) } ) -> ( B e. _V <-> ( A X. B ) e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		bj-xpexg2	|- ( A e. ( V \ { (/) } ) -> ( B e. _V -> ( A X. B ) e. _V ) )
2		eldifsni	|- ( A e. ( V \ { (/) } ) -> A =/= (/) )
3		bj-xpnzex	|- ( A =/= (/) -> ( ( A X. B ) e. _V -> B e. _V ) )
4	2 3	syl	|- ( A e. ( V \ { (/) } ) -> ( ( A X. B ) e. _V -> B e. _V ) )
5	1 4	impbid	|- ( A e. ( V \ { (/) } ) -> ( B e. _V <-> ( A X. B ) e. _V ) )