Theorem dmxpid 5833

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 5823	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5599	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5680	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2794	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5808	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 22	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2804	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5832	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3028	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

Syntax hints:   = wceq 1539  ∅c0 4257   × cxp 5583  dom cdm 5585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5222  ax-nul 5229  ax-pr 5351

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rab 3073  df-v 3432  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5075  df-opab 5137  df-xp 5591  df-dm 5595

This theorem is referenced by:  dmxpin  5834  xpid11  5835  sofld  6084  xpider  8565  hartogslem1  9289  unxpwdom2  9335  infxpenlem  9757  fpwwe2lem12  10386  fpwwe2  10387  canth4  10391  dmrecnq  10712  homfeqbas  17393  sscfn1  17517  sscfn2  17518  ssclem  17519  isssc  17520  rescval2  17528  issubc2  17539  cofuval  17585  resfval2  17596  resf1st  17597  psssdm2  18287  tsrss  18295  decpmatval  21902  pmatcollpw3lem  21920  ustssco  23354  ustbas2  23365  psmetdmdm  23446  xmetdmdm  23476  setsmstopn  23621  tmsval  23624  tngtopn  23802  caufval  24427  grporndm  28858  dfhnorm2  29470  hhshsslem1  29615  metideq  31829  filnetlem4  34556  poimirlem3  35766  ssbnd  35932  bnd2lem  35935  ismtyval  35944  ismndo2  36018  exidreslem  36021  divrngcl  36101  isdrngo2  36102  rtrclex  41184  fnxpdmdm  45278