Metamath Proof Explorer


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