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 5955

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 5945	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5714	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5798	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2796	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5930	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 22	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2806	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5953	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3031	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

Colors of variables: wff setvar class

Syntax hints: = wceq 1537 ∅c0 4352 × cxp 5698 dom cdm 5700

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pr 5447

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-sb 2065 df-clab 2718 df-cleq 2732 df-clel 2819 df-ne 2947 df-ral 3068 df-rex 3077 df-rab 3444 df-v 3490 df-dif 3979 df-un 3981 df-ss 3993 df-nul 4353 df-if 4549 df-sn 4649 df-pr 4651 df-op 4655 df-br 5167 df-opab 5229 df-xp 5706 df-dm 5710

This theorem is referenced by: dmxpin 5956 xpid11 5957 sofld 6218 xpider 8846 hartogslem1 9611 unxpwdom2 9657 infxpenlem 10082 fpwwe2lem12 10711 fpwwe2 10712 canth4 10716 dmrecnq 11037 homfeqbas 17754 sscfn1 17878 sscfn2 17879 ssclem 17880 isssc 17881 rescval2 17889 issubc2 17900 cofuval 17946 resfval2 17957 resf1st 17958 psssdm2 18651 tsrss 18659 decpmatval 22792 pmatcollpw3lem 22810 ustssco 24244 ustbas2 24255 psmetdmdm 24336 xmetdmdm 24366 setsmstopn 24511 tmsval 24514 tngtopn 24692 caufval 25328 grporndm 30542 dfhnorm2 31154 hhshsslem1 31299 metideq 33839 filnetlem4 36347 poimirlem3 37583 ssbnd 37748 bnd2lem 37751 ismtyval 37760 ismndo2 37834 exidreslem 37837 divrngcl 37917 isdrngo2 37918 rtrclex 43579 fnxpdmdm 47883