Theorem dmxpid 5907

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 5897	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5662	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5747	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2814	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5882	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 22	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2824	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5906	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3041	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

Syntax hints:   = wceq 1561  ∅c0 4286   × cxp 5646  dom cdm 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5247  ax-pr 5391

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5102  df-opab 5164  df-xp 5654  df-dm 5658

This theorem is referenced by:  dmxpin  5908  xpid11  5909  sofld  6173  xpider  8770  hartogslem1  9488  unxpwdom2  9534  infxpenlem  9981  fpwwe2lem12  10611  fpwwe2  10612  canth4  10616  dmrecnq  10937  homfeqbas  17738  sscfn1  17860  sscfn2  17861  ssclem  17862  isssc  17863  rescval2  17871  issubc2  17879  cofuval  17925  resfval2  17936  resf1st  17937  psssdm2  18623  tsrss  18631  decpmatval  22832  pmatcollpw3lem  22850  ustssco  24282  ustbas2  24292  psmetdmdm  24372  xmetdmdm  24402  setsmstopn  24545  tmsval  24548  tngtopn  24717  caufval  25344  grporndm  30720  dfhnorm2  31332  hhshsslem1  31477  metideq  34192  filnetlem4  36746  poimirlem3  38127  ssbnd  38292  bnd2lem  38295  ismtyval  38304  ismndo2  38378  exidreslem  38381  divrngcl  38461  isdrngo2  38462  rtrclex  44198  fnxpdmdm  48773  dmdm  49665  infsubc2d  49674