Theorem dmxpid 5896

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 5886	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5654	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5739	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2781	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5871	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 22	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2791	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5894	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3009	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

Syntax hints:   = wceq 1540  ∅c0 4298   × cxp 5638  dom cdm 5640

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 2702  ax-sep 5253  ax-nul 5263  ax-pr 5389

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-br 5110  df-opab 5172  df-xp 5646  df-dm 5650

This theorem is referenced by:  dmxpin  5897  xpid11  5898  sofld  6162  xpider  8763  hartogslem1  9501  unxpwdom2  9547  infxpenlem  9972  fpwwe2lem12  10601  fpwwe2  10602  canth4  10606  dmrecnq  10927  homfeqbas  17663  sscfn1  17785  sscfn2  17786  ssclem  17787  isssc  17788  rescval2  17796  issubc2  17804  cofuval  17850  resfval2  17861  resf1st  17862  psssdm2  18546  tsrss  18554  decpmatval  22658  pmatcollpw3lem  22676  ustssco  24108  ustbas2  24119  psmetdmdm  24199  xmetdmdm  24229  setsmstopn  24372  tmsval  24375  tngtopn  24544  caufval  25181  grporndm  30445  dfhnorm2  31057  hhshsslem1  31202  metideq  33889  filnetlem4  36364  poimirlem3  37612  ssbnd  37777  bnd2lem  37780  ismtyval  37789  ismndo2  37863  exidreslem  37866  divrngcl  37946  isdrngo2  37947  rtrclex  43599  fnxpdmdm  48138  dmdm  49032  infsubc2d  49041