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\in V\to \left(B\in W\to A\times tagB\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢B\in W\to B\in \mathrm{V}$$
2		bj-tagex	$$⊢B\in \mathrm{V}\leftrightarrow tagB\in \mathrm{V}$$
3	1 2	sylib	$$⊢B\in W\to tagB\in \mathrm{V}$$
4		bj-xpexg2	$$⊢A\in V\to \left(tagB\in \mathrm{V}\to A\times tagB\in \mathrm{V}\right)$$
5	3 4	syl5	$$⊢A\in V\to \left(B\in W\to A\times tagB\in \mathrm{V}\right)$$