Metamath Proof Explorer


Theorem bj-xpexg2

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

Ref Expression
Assertion bj-xpexg2 AVBWA×BV

Proof

Step Hyp Ref Expression
1 xpexg AVBWA×BV
2 1 ex AVBWA×BV