Theorem dmxpid 5920

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 5910	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5675	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5760	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2812	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5895	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 23	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2822	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5919	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3039	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

Syntax hints:   = wceq 1568  ∅c0 4285   × cxp 5659  dom cdm 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5256  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-xp 5667  df-dm 5671

This theorem is referenced by:  dmxpin  5921  xpid11  5922  sofld  6185  xpider  8785  hartogslem1  9503  unxpwdom2  9549  infxpenlem  9996  fpwwe2lem12  10626  fpwwe2  10627  canth4  10631  dmrecnq  10952  homfeqbas  17751  sscfn1  17873  sscfn2  17874  ssclem  17875  isssc  17876  rescval2  17884  issubc2  17892  cofuval  17938  resfval2  17949  resf1st  17950  psssdm2  18636  tsrss  18644  decpmatval  22901  pmatcollpw3lem  22919  ustssco  24351  ustbas2  24361  psmetdmdm  24441  xmetdmdm  24471  setsmstopn  24614  tmsval  24617  tngtopn  24786  caufval  25413  grporndm  30828  dfhnorm2  31440  hhshsslem1  31585  metideq  34249  filnetlem4  36836  poimirlem3  38218  ssbnd  38383  bnd2lem  38386  ismtyval  38395  ismndo2  38469  exidreslem  38472  divrngcl  38552  isdrngo2  38553  rtrclex  44291  fnxpdmdm  48870  dmdm  49776  infsubc2d  49785