Metamath Proof Explorer


Theorem unixp

Description: The double class union of a nonempty Cartesian product is the union of it members. (Contributed by NM, 17-Sep-2006)

Ref Expression
Assertion unixp A × B A × B = A B

Proof

Step Hyp Ref Expression
1 relxp Rel A × B
2 relfld Rel A × B A × B = dom A × B ran A × B
3 1 2 ax-mp A × B = dom A × B ran A × B
4 xpeq2 B = A × B = A ×
5 xp0 A × =
6 4 5 eqtrdi B = A × B =
7 6 necon3i A × B B
8 xpeq1 A = A × B = × B
9 0xp × B =
10 8 9 eqtrdi A = A × B =
11 10 necon3i A × B A
12 dmxp B dom A × B = A
13 rnxp A ran A × B = B
14 uneq12 dom A × B = A ran A × B = B dom A × B ran A × B = A B
15 12 13 14 syl2an B A dom A × B ran A × B = A B
16 7 11 15 syl2anc A × B dom A × B ran A × B = A B
17 3 16 eqtrid A × B A × B = A B