Description: The Cartesian square of a set is a set. (Contributed by AV, 13-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | sqxpexg | |- ( A e. V -> ( A X. A ) e. _V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpexg | |- ( ( A e. V /\ A e. V ) -> ( A X. A ) e. _V ) |
|
2 | 1 | anidms | |- ( A e. V -> ( A X. A ) e. _V ) |