Theorem dmxpid 5876

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 5867	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5637	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5722	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2780	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5852	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 22	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2790	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5875	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3008	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

Syntax hints:   = wceq 1540  ∅c0 4286   × cxp 5621  dom cdm 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629  df-dm 5633

This theorem is referenced by:  dmxpin  5877  xpid11  5878  sofld  6140  xpider  8722  hartogslem1  9453  unxpwdom2  9499  infxpenlem  9926  fpwwe2lem12  10555  fpwwe2  10556  canth4  10560  dmrecnq  10881  homfeqbas  17620  sscfn1  17742  sscfn2  17743  ssclem  17744  isssc  17745  rescval2  17753  issubc2  17761  cofuval  17807  resfval2  17818  resf1st  17819  psssdm2  18505  tsrss  18513  decpmatval  22668  pmatcollpw3lem  22686  ustssco  24118  ustbas2  24129  psmetdmdm  24209  xmetdmdm  24239  setsmstopn  24382  tmsval  24385  tngtopn  24554  caufval  25191  grporndm  30472  dfhnorm2  31084  hhshsslem1  31229  metideq  33859  filnetlem4  36354  poimirlem3  37602  ssbnd  37767  bnd2lem  37770  ismtyval  37779  ismndo2  37853  exidreslem  37856  divrngcl  37936  isdrngo2  37937  rtrclex  43590  fnxpdmdm  48132  dmdm  49026  infsubc2d  49035