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	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 ∈ 𝑊 → ( 𝐴 × tag 𝐵 ) ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ V )
2		bj-tagex	⊢ ( 𝐵 ∈ V ↔ tag 𝐵 ∈ V )
3	1 2	sylib	⊢ ( 𝐵 ∈ 𝑊 → tag 𝐵 ∈ V )
4		bj-xpexg2	⊢ ( 𝐴 ∈ 𝑉 → ( tag 𝐵 ∈ V → ( 𝐴 × tag 𝐵 ) ∈ V ) )
5	3 4	syl5	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 ∈ 𝑊 → ( 𝐴 × tag 𝐵 ) ∈ V ) )