dmxpid - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dmxpid		Structured version Visualization version GIF version

Theorem dmxpid 5943

Description: The domain of a Cartesian square. (Contributed by NM, 28-Jul-1995.)

**Assertion**
Ref	Expression
dmxpid	⊢ dom (𝐴 × 𝐴) = 𝐴

**Proof of Theorem dmxpid**
Step	Hyp	Ref	Expression
1		dm0 5933	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5702	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5786	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2790	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5918	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 22	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2800	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5941	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3022	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

Colors of variables: wff setvar class

Syntax hints: = wceq 1536 ∅c0 4338 × cxp 5686 dom cdm 5688

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-ne 2938 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5148 df-opab 5210 df-xp 5694 df-dm 5698

This theorem is referenced by: dmxpin 5944 xpid11 5945 sofld 6208 xpider 8826 hartogslem1 9579 unxpwdom2 9625 infxpenlem 10050 fpwwe2lem12 10679 fpwwe2 10680 canth4 10684 dmrecnq 11005 homfeqbas 17740 sscfn1 17864 sscfn2 17865 ssclem 17866 isssc 17867 rescval2 17875 issubc2 17886 cofuval 17932 resfval2 17943 resf1st 17944 psssdm2 18638 tsrss 18646 decpmatval 22786 pmatcollpw3lem 22804 ustssco 24238 ustbas2 24249 psmetdmdm 24330 xmetdmdm 24360 setsmstopn 24505 tmsval 24508 tngtopn 24686 caufval 25322 grporndm 30538 dfhnorm2 31150 hhshsslem1 31295 metideq 33853 filnetlem4 36363 poimirlem3 37609 ssbnd 37774 bnd2lem 37777 ismtyval 37786 ismndo2 37860 exidreslem 37863 divrngcl 37943 isdrngo2 37944 rtrclex 43606 fnxpdmdm 48003