Theorem dmxpid 5880

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 5870	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5639	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5724	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2788	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5855	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 22	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2798	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5879	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3016	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

Syntax hints:   = wceq 1542  ∅c0 4286   × cxp 5623  dom cdm 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-xp 5631  df-dm 5635

This theorem is referenced by:  dmxpin  5881  xpid11  5882  sofld  6146  xpider  8730  hartogslem1  9452  unxpwdom2  9498  infxpenlem  9928  fpwwe2lem12  10558  fpwwe2  10559  canth4  10563  dmrecnq  10884  homfeqbas  17624  sscfn1  17746  sscfn2  17747  ssclem  17748  isssc  17749  rescval2  17757  issubc2  17765  cofuval  17811  resfval2  17822  resf1st  17823  psssdm2  18509  tsrss  18517  decpmatval  22714  pmatcollpw3lem  22732  ustssco  24164  ustbas2  24174  psmetdmdm  24254  xmetdmdm  24284  setsmstopn  24427  tmsval  24430  tngtopn  24599  caufval  25236  grporndm  30590  dfhnorm2  31202  hhshsslem1  31347  metideq  34063  filnetlem4  36588  poimirlem3  37837  ssbnd  38002  bnd2lem  38005  ismtyval  38014  ismndo2  38088  exidreslem  38091  divrngcl  38171  isdrngo2  38172  rtrclex  43936  fnxpdmdm  48483  dmdm  49375  infsubc2d  49384