Metamath Proof Explorer


Theorem dmxpss

Description: The domain of a Cartesian product is included in its first factor. (Contributed by NM, 19-Mar-2007)

Ref Expression
Assertion dmxpss dom A × B A

Proof

Step Hyp Ref Expression
1 xpeq2 B = A × B = A ×
2 xp0 A × =
3 1 2 eqtrdi B = A × B =
4 3 dmeqd B = dom A × B = dom
5 dm0 dom =
6 4 5 eqtrdi B = dom A × B =
7 0ss A
8 6 7 eqsstrdi B = dom A × B A
9 dmxp B dom A × B = A
10 eqimss dom A × B = A dom A × B A
11 9 10 syl B dom A × B A
12 8 11 pm2.61ine dom A × B A