Theorem dmxpid 5875

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 5865	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5633	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5718	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2782	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5850	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 22	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2792	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5874	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3011	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

Syntax hints:   = wceq 1541  ∅c0 4282   × cxp 5617  dom cdm 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-xp 5625  df-dm 5629

This theorem is referenced by:  dmxpin  5876  xpid11  5877  sofld  6140  xpider  8718  hartogslem1  9434  unxpwdom2  9480  infxpenlem  9910  fpwwe2lem12  10539  fpwwe2  10540  canth4  10544  dmrecnq  10865  homfeqbas  17608  sscfn1  17730  sscfn2  17731  ssclem  17732  isssc  17733  rescval2  17741  issubc2  17749  cofuval  17795  resfval2  17806  resf1st  17807  psssdm2  18493  tsrss  18501  decpmatval  22686  pmatcollpw3lem  22704  ustssco  24136  ustbas2  24146  psmetdmdm  24226  xmetdmdm  24256  setsmstopn  24399  tmsval  24402  tngtopn  24571  caufval  25208  grporndm  30497  dfhnorm2  31109  hhshsslem1  31254  metideq  33913  filnetlem4  36432  poimirlem3  37669  ssbnd  37834  bnd2lem  37837  ismtyval  37846  ismndo2  37920  exidreslem  37923  divrngcl  38003  isdrngo2  38004  rtrclex  43715  fnxpdmdm  48265  dmdm  49159  infsubc2d  49168