Metamath Proof Explorer


Theorem bj-xpexg2

Description: Curried (exported) form of xpexg . (Contributed by BJ, 2-Apr-2019)

Ref Expression
Assertion bj-xpexg2 A V B W A × B V

Proof

Step Hyp Ref Expression
1 xpexg A V B W A × B V
2 1 ex A V B W A × B V