Theorem dmxpid 5908

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 5898	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5661	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5746	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2811	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5883	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 23	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2821	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5907	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3038	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

This proof depends on syntax axioms:   = wceq 1570  ∅c0 4278   × cxp 5645  dom cdm 5647

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-xp 5653  df-dm 5657

This theorem is used by:  dmxpin  5909  xpid11  5910  sofld  6174  xpider  8787  hartogslem1  9514  unxpwdom2  9560  infxpenlem  10063  fpwwe2lem12  10698  fpwwe2  10699  canth4  10703  dmrecnq  11024  homfeqbas  17831  sscfn1  17953  sscfn2  17954  ssclem  17955  isssc  17956  rescval2  17964  issubc2  17972  cofuval  18018  resfval2  18029  resf1st  18030  psssdm2  18716  tsrss  18724  decpmatval  23044  pmatcollpw3lem  23062  ustssco  24495  ustbas2  24505  psmetdmdm  24585  xmetdmdm  24615  setsmstopn  24758  tmsval  24761  tngtopn  24930  caufval  25557  grporndm  31045  dfhnorm2  31657  hhshsslem1  31802  metideq  34458  filnetlem4  37091  poimirlem3  38461  ssbnd  38642  bnd2lem  38645  ismtyval  38654  ismndo2  38728  exidreslem  38731  divrngcl  38811  isdrngo2  38812  rtrclex  44561  fnxpdmdm  49179  dmdm  50083  infsubc2d  50092