Theorem dmxpid 5931

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 5922	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5691	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5775	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2781	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5907	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 22	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2791	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5930	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3015	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

Syntax hints:   = wceq 1533  ∅c0 4323   × cxp 5675  dom cdm 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5299  ax-nul 5306  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rab 3420  df-v 3465  df-dif 3948  df-un 3950  df-ss 3962  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5149  df-opab 5211  df-xp 5683  df-dm 5687

This theorem is referenced by:  dmxpin  5932  xpid11  5933  sofld  6191  xpider  8805  hartogslem1  9565  unxpwdom2  9611  infxpenlem  10036  fpwwe2lem12  10665  fpwwe2  10666  canth4  10670  dmrecnq  10991  homfeqbas  17675  sscfn1  17799  sscfn2  17800  ssclem  17801  isssc  17802  rescval2  17810  issubc2  17821  cofuval  17867  resfval2  17878  resf1st  17879  psssdm2  18572  tsrss  18580  decpmatval  22697  pmatcollpw3lem  22715  ustssco  24149  ustbas2  24160  psmetdmdm  24241  xmetdmdm  24271  setsmstopn  24416  tmsval  24419  tngtopn  24597  caufval  25233  grporndm  30376  dfhnorm2  30988  hhshsslem1  31133  metideq  33564  filnetlem4  35935  poimirlem3  37166  ssbnd  37331  bnd2lem  37334  ismtyval  37343  ismndo2  37417  exidreslem  37420  divrngcl  37500  isdrngo2  37501  rtrclex  43112  fnxpdmdm  47334