Metamath Proof Explorer


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 A A × B V B V

Proof

Step Hyp Ref Expression
1 0ex V
2 eleq1a V B = B V
3 1 2 ax-mp B = B V
4 3 a1d B = A × B V B V
5 4 a1d B = A A × B V B V
6 xpnz A B A × B
7 xpexr2 A × B V A × B A V B V
8 7 simprd A × B V A × B B V
9 8 expcom A × B A × B V B V
10 6 9 sylbi A B A × B V B V
11 10 expcom B A A × B V B V
12 5 11 pm2.61ine A A × B V B V