Theorem dmxpid 5895

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 5885	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5650	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5735	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2803	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5870	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 22	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2813	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5894	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3030	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

Syntax hints:   = wceq 1550  ∅c0 4276   × cxp 5634  dom cdm 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-sep 5236  ax-pr 5380

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ne 2948  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-br 5091  df-opab 5153  df-xp 5642  df-dm 5646

This theorem is referenced by:  dmxpin  5896  xpid11  5897  sofld  6158  xpider  8754  hartogslem1  9476  unxpwdom2  9522  infxpenlem  9955  fpwwe2lem12  10586  fpwwe2  10587  canth4  10591  dmrecnq  10912  homfeqbas  17700  sscfn1  17822  sscfn2  17823  ssclem  17824  isssc  17825  rescval2  17833  issubc2  17841  cofuval  17887  resfval2  17898  resf1st  17899  psssdm2  18585  tsrss  18593  decpmatval  22794  pmatcollpw3lem  22812  ustssco  24244  ustbas2  24254  psmetdmdm  24334  xmetdmdm  24364  setsmstopn  24507  tmsval  24510  tngtopn  24679  caufval  25306  grporndm  30648  dfhnorm2  31260  hhshsslem1  31405  metideq  34134  filnetlem4  36679  poimirlem3  38060  ssbnd  38225  bnd2lem  38228  ismtyval  38237  ismndo2  38311  exidreslem  38314  divrngcl  38394  isdrngo2  38395  rtrclex  44131  fnxpdmdm  48720  dmdm  49612  infsubc2d  49621