Theorem dmxpid 5918

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 5908	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5673	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5758	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2813	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5893	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 23	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2823	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5917	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3040	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

This proof depends on syntax axioms:   = wceq 1570  ∅c0 4282   × cxp 5657  dom cdm 5659

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 2734  ax-sep 5255  ax-pr 5402

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-xp 5665  df-dm 5669

This theorem is used by:  dmxpin  5919  xpid11  5920  sofld  6184  xpider  8791  hartogslem1  9517  unxpwdom2  9563  infxpenlem  10019  fpwwe2lem12  10654  fpwwe2  10655  canth4  10659  dmrecnq  10980  homfeqbas  17788  sscfn1  17910  sscfn2  17911  ssclem  17912  isssc  17913  rescval2  17921  issubc2  17929  cofuval  17975  resfval2  17986  resf1st  17987  psssdm2  18673  tsrss  18681  decpmatval  22991  pmatcollpw3lem  23009  ustssco  24442  ustbas2  24452  psmetdmdm  24532  xmetdmdm  24562  setsmstopn  24705  tmsval  24708  tngtopn  24877  caufval  25504  grporndm  30977  dfhnorm2  31589  hhshsslem1  31734  metideq  34390  filnetlem4  36987  poimirlem3  38359  ssbnd  38525  bnd2lem  38528  ismtyval  38537  ismndo2  38611  exidreslem  38614  divrngcl  38694  isdrngo2  38695  rtrclex  44444  fnxpdmdm  49062  dmdm  49966  infsubc2d  49975