Theorem dmxpid 5874

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 5864	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5634	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5719	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2786	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5849	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 22	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2796	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5873	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3013	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

Syntax hints:   = wceq 1542  ∅c0 4263   × cxp 5618  dom cdm 5620

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 2707  ax-sep 5220  ax-pr 5364

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 2714  df-cleq 2727  df-clel 2810  df-ne 2931  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-opab 5137  df-xp 5626  df-dm 5630

This theorem is referenced by:  dmxpin  5875  xpid11  5876  sofld  6140  xpider  8724  hartogslem1  9446  unxpwdom2  9492  infxpenlem  9924  fpwwe2lem12  10554  fpwwe2  10555  canth4  10559  dmrecnq  10880  homfeqbas  17651  sscfn1  17773  sscfn2  17774  ssclem  17775  isssc  17776  rescval2  17784  issubc2  17792  cofuval  17838  resfval2  17849  resf1st  17850  psssdm2  18536  tsrss  18544  decpmatval  22718  pmatcollpw3lem  22736  ustssco  24168  ustbas2  24178  psmetdmdm  24258  xmetdmdm  24288  setsmstopn  24431  tmsval  24434  tngtopn  24603  caufval  25230  grporndm  30569  dfhnorm2  31181  hhshsslem1  31326  metideq  34025  filnetlem4  36551  poimirlem3  37932  ssbnd  38097  bnd2lem  38100  ismtyval  38109  ismndo2  38183  exidreslem  38186  divrngcl  38266  isdrngo2  38267  rtrclex  44032  fnxpdmdm  48624  dmdm  49516  infsubc2d  49525