Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
"Singletonization" and tagging
bj-xtagex
Next ⟩
Tuples of classes
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-xtagex
Description:
The product of a set and the tagging of a set is a set.
(Contributed by
BJ
, 2-Apr-2019)
Ref
Expression
Assertion
bj-xtagex
⊢
A
∈
V
→
B
∈
W
→
A
×
tag
B
∈
V
Proof
Step
Hyp
Ref
Expression
1
elex
⊢
B
∈
W
→
B
∈
V
2
bj-tagex
⊢
B
∈
V
↔
tag
B
∈
V
3
1
2
sylib
⊢
B
∈
W
→
tag
B
∈
V
4
bj-xpexg2
⊢
A
∈
V
→
tag
B
∈
V
→
A
×
tag
B
∈
V
5
3
4
syl5
⊢
A
∈
V
→
B
∈
W
→
A
×
tag
B
∈
V