Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
Complements on direct products
bj-xpexg2
Next ⟩
bj-xpnzexb
Metamath Proof Explorer
Ascii
Unicode
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