Theorem dmxpid 5897

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

Syntax hints:   = wceq 1540  ∅c0 4299   × cxp 5639  dom cdm 5641

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 5254  ax-nul 5264  ax-pr 5390

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 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-dm 5651

This theorem is referenced by:  dmxpin  5898  xpid11  5899  sofld  6163  xpider  8764  hartogslem1  9502  unxpwdom2  9548  infxpenlem  9973  fpwwe2lem12  10602  fpwwe2  10603  canth4  10607  dmrecnq  10928  homfeqbas  17664  sscfn1  17786  sscfn2  17787  ssclem  17788  isssc  17789  rescval2  17797  issubc2  17805  cofuval  17851  resfval2  17862  resf1st  17863  psssdm2  18547  tsrss  18555  decpmatval  22659  pmatcollpw3lem  22677  ustssco  24109  ustbas2  24120  psmetdmdm  24200  xmetdmdm  24230  setsmstopn  24373  tmsval  24376  tngtopn  24545  caufval  25182  grporndm  30446  dfhnorm2  31058  hhshsslem1  31203  metideq  33890  filnetlem4  36376  poimirlem3  37624  ssbnd  37789  bnd2lem  37792  ismtyval  37801  ismndo2  37875  exidreslem  37878  divrngcl  37958  isdrngo2  37959  rtrclex  43613  fnxpdmdm  48152  dmdm  49046  infsubc2d  49055