Theorem bj-xpnzex

Description: If the first factor of a product is nonempty, and the product is a set, then the second factor is a set. UPDATE: this is actually the curried (exported) form of xpexcnv (up to commutation in the product). (Contributed by BJ, 6-Oct-2018) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-xpnzex	⊢ ( 𝐴 ≠ ∅ → ( ( 𝐴 × 𝐵 ) ∈ 𝑉 → 𝐵 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		eleq1a	⊢ ( ∅ ∈ V → ( 𝐵 = ∅ → 𝐵 ∈ V ) )
3	1 2	ax-mp	⊢ ( 𝐵 = ∅ → 𝐵 ∈ V )
4	3	a1d	⊢ ( 𝐵 = ∅ → ( ( 𝐴 × 𝐵 ) ∈ 𝑉 → 𝐵 ∈ V ) )
5	4	a1d	⊢ ( 𝐵 = ∅ → ( 𝐴 ≠ ∅ → ( ( 𝐴 × 𝐵 ) ∈ 𝑉 → 𝐵 ∈ V ) ) )
6		xpnz	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( 𝐴 × 𝐵 ) ≠ ∅ )
7		xpexr2	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ 𝑉 ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
8	7	simprd	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ 𝑉 ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → 𝐵 ∈ V )
9	8	expcom	⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( ( 𝐴 × 𝐵 ) ∈ 𝑉 → 𝐵 ∈ V ) )
10	6 9	sylbi	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ∈ 𝑉 → 𝐵 ∈ V ) )
11	10	expcom	⊢ ( 𝐵 ≠ ∅ → ( 𝐴 ≠ ∅ → ( ( 𝐴 × 𝐵 ) ∈ 𝑉 → 𝐵 ∈ V ) ) )
12	5 11	pm2.61ine	⊢ ( 𝐴 ≠ ∅ → ( ( 𝐴 × 𝐵 ) ∈ 𝑉 → 𝐵 ∈ V ) )