**Description:** The Cartesian product of two sets is a set. (Contributed by Glauco
Siliprandi, 26-Jun-2021)

Ref | Expression | ||
---|---|---|---|

Hypotheses | xpexd.1 | $${\u22a2}{\phi}\to {A}\in {V}$$ | |

xpexd.2 | $${\u22a2}{\phi}\to {B}\in {W}$$ | ||

Assertion | xpexd | $${\u22a2}{\phi}\to {A}\times {B}\in \mathrm{V}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | xpexd.1 | $${\u22a2}{\phi}\to {A}\in {V}$$ | |

2 | xpexd.2 | $${\u22a2}{\phi}\to {B}\in {W}$$ | |

3 | xpexg | $${\u22a2}\left({A}\in {V}\wedge {B}\in {W}\right)\to {A}\times {B}\in \mathrm{V}$$ | |

4 | 1 2 3 | syl2anc | $${\u22a2}{\phi}\to {A}\times {B}\in \mathrm{V}$$ |