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 e. V -> ( B e. W -> ( A X. tag B ) e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( B e. W -> B e. _V )
2		bj-tagex	|- ( B e. _V <-> tag B e. _V )
3	1 2	sylib	|- ( B e. W -> tag B e. _V )
4		bj-xpexg2	|- ( A e. V -> ( tag B e. _V -> ( A X. tag B ) e. _V ) )
5	3 4	syl5	|- ( A e. V -> ( B e. W -> ( A X. tag B ) e. _V ) )