Metamath Proof Explorer

Theorem bj-xpexg2

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

Ref Expression
Assertion bj-xpexg2 
|- ( A e. V -> ( B e. W -> ( A X. B ) e. _V ) )

Proof

Step Hyp Ref Expression
1 xpexg 
 |-  ( ( A e. V /\ B e. W ) -> ( A X. B ) e. _V )
2 1 ex 
 |-  ( A e. V -> ( B e. W -> ( A X. B ) e. _V ) )