Theorem dmxpid 5828

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 5818	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5594	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5675	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2795	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5803	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 22	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2805	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5827	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3027	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

Syntax hints:   = wceq 1539  ∅c0 4253   × cxp 5578  dom cdm 5580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-dm 5590

This theorem is referenced by:  dmxpin  5829  xpid11  5830  sofld  6079  xpider  8535  hartogslem1  9231  unxpwdom2  9277  infxpenlem  9700  fpwwe2lem12  10329  fpwwe2  10330  canth4  10334  dmrecnq  10655  homfeqbas  17322  sscfn1  17446  sscfn2  17447  ssclem  17448  isssc  17449  rescval2  17457  issubc2  17467  cofuval  17513  resfval2  17524  resf1st  17525  psssdm2  18214  tsrss  18222  decpmatval  21822  pmatcollpw3lem  21840  ustssco  23274  ustbas2  23285  psmetdmdm  23366  xmetdmdm  23396  setsmstopn  23539  tmsval  23542  tngtopn  23720  caufval  24344  grporndm  28773  dfhnorm2  29385  hhshsslem1  29530  metideq  31745  filnetlem4  34497  poimirlem3  35707  ssbnd  35873  bnd2lem  35876  ismtyval  35885  ismndo2  35959  exidreslem  35962  divrngcl  36042  isdrngo2  36043  rtrclex  41114  fnxpdmdm  45210