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  17676  sscfn1  17800  sscfn2  17801  ssclem  17802  isssc  17803  rescval2  17811  issubc2  17822  cofuval  17868  resfval2  17879  resf1st  17880  psssdm2  18573  tsrss  18581  decpmatval  22698  pmatcollpw3lem  22716  ustssco  24150  ustbas2  24161  psmetdmdm  24242  xmetdmdm  24272  setsmstopn  24417  tmsval  24420  tngtopn  24598  caufval  25234  grporndm  30377  dfhnorm2  30989  hhshsslem1  31134  metideq  33581  filnetlem4  35952  poimirlem3  37183  ssbnd  37348  bnd2lem  37351  ismtyval  37360  ismndo2  37434  exidreslem  37437  divrngcl  37517  isdrngo2  37518  rtrclex  43129  fnxpdmdm  47350