Theorem dmxpid 5932

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 5923	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5692	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5776	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2781	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5908	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 22	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2791	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5931	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3014	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

Syntax hints:   = wceq 1533  ∅c0 4322   × cxp 5676  dom cdm 5678

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 5300  ax-nul 5307  ax-pr 5429

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 2930  df-ral 3051  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-opab 5212  df-xp 5684  df-dm 5688

This theorem is referenced by:  dmxpin  5933  xpid11  5934  sofld  6193  xpider  8807  hartogslem1  9567  unxpwdom2  9613  infxpenlem  10038  fpwwe2lem12  10667  fpwwe2  10668  canth4  10672  dmrecnq  10993  homfeqbas  17679  sscfn1  17803  sscfn2  17804  ssclem  17805  isssc  17806  rescval2  17814  issubc2  17825  cofuval  17871  resfval2  17882  resf1st  17883  psssdm2  18576  tsrss  18584  decpmatval  22711  pmatcollpw3lem  22729  ustssco  24163  ustbas2  24174  psmetdmdm  24255  xmetdmdm  24285  setsmstopn  24430  tmsval  24433  tngtopn  24611  caufval  25247  grporndm  30392  dfhnorm2  31004  hhshsslem1  31149  metideq  33625  filnetlem4  35996  poimirlem3  37227  ssbnd  37392  bnd2lem  37395  ismtyval  37404  ismndo2  37478  exidreslem  37481  divrngcl  37561  isdrngo2  37562  rtrclex  43189  fnxpdmdm  47408