Theorem dmxpid 5904

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 5894	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5659	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5744	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2812	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5879	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 22	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2822	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5903	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3039	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

Syntax hints:   = wceq 1559  ∅c0 4285   × cxp 5643  dom cdm 5645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-xp 5651  df-dm 5655

This theorem is referenced by:  dmxpin  5905  xpid11  5906  sofld  6167  xpider  8763  hartogslem1  9485  unxpwdom2  9531  infxpenlem  9964  fpwwe2lem12  10595  fpwwe2  10596  canth4  10600  dmrecnq  10921  homfeqbas  17709  sscfn1  17831  sscfn2  17832  ssclem  17833  isssc  17834  rescval2  17842  issubc2  17850  cofuval  17896  resfval2  17907  resf1st  17908  psssdm2  18594  tsrss  18602  decpmatval  22803  pmatcollpw3lem  22821  ustssco  24253  ustbas2  24263  psmetdmdm  24343  xmetdmdm  24373  setsmstopn  24516  tmsval  24519  tngtopn  24688  caufval  25315  grporndm  30657  dfhnorm2  31269  hhshsslem1  31414  metideq  34149  filnetlem4  36694  poimirlem3  38075  ssbnd  38240  bnd2lem  38243  ismtyval  38252  ismndo2  38326  exidreslem  38329  divrngcl  38409  isdrngo2  38410  rtrclex  44146  fnxpdmdm  48735  dmdm  49627  infsubc2d  49636