Theorem dmxpid 5894

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

Syntax hints:   = wceq 1540  ∅c0 4296   × cxp 5636  dom cdm 5638

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-dm 5648

This theorem is referenced by:  dmxpin  5895  xpid11  5896  sofld  6160  xpider  8761  hartogslem1  9495  unxpwdom2  9541  infxpenlem  9966  fpwwe2lem12  10595  fpwwe2  10596  canth4  10600  dmrecnq  10921  homfeqbas  17657  sscfn1  17779  sscfn2  17780  ssclem  17781  isssc  17782  rescval2  17790  issubc2  17798  cofuval  17844  resfval2  17855  resf1st  17856  psssdm2  18540  tsrss  18548  decpmatval  22652  pmatcollpw3lem  22670  ustssco  24102  ustbas2  24113  psmetdmdm  24193  xmetdmdm  24223  setsmstopn  24366  tmsval  24369  tngtopn  24538  caufval  25175  grporndm  30439  dfhnorm2  31051  hhshsslem1  31196  metideq  33883  filnetlem4  36369  poimirlem3  37617  ssbnd  37782  bnd2lem  37785  ismtyval  37794  ismndo2  37868  exidreslem  37871  divrngcl  37951  isdrngo2  37952  rtrclex  43606  fnxpdmdm  48148  dmdm  49042  infsubc2d  49051