Theorem dmxpid 5919

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 5909	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5669	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5755	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2814	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5894	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 23	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2824	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5918	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3042	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

This proof depends on syntax axioms:   = wceq 1570  ∅c0 4281   × cxp 5653  dom cdm 5655

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-dm 5665

This theorem is used by:  dmxpin  5920  xpid11  5921  sofld  6191  xpider  8837  hartogslem1  9563  unxpwdom2  9609  infxpenlem  10119  fpwwe2lem12  10754  fpwwe2  10755  canth4  10759  dmrecnq  11080  homfeqbas  17899  sscfn1  18021  sscfn2  18022  ssclem  18023  isssc  18024  rescval2  18032  issubc2  18040  cofuval  18086  resfval2  18097  resf1st  18098  psssdm2  18784  tsrss  18792  decpmatval  23113  pmatcollpw3lem  23131  ustssco  24564  ustbas2  24574  psmetdmdm  24654  xmetdmdm  24684  setsmstopn  24827  tmsval  24830  tngtopn  24999  caufval  25626  grporndm  31142  dfhnorm2  31754  hhshsslem1  31899  metideq  34595  filnetlem4  37347  poimirlem3  38733  ssbnd  38914  bnd2lem  38917  ismtyval  38926  ismndo2  39000  exidreslem  39003  divrngcl  39083  isdrngo2  39084  rtrclex  44809  fnxpdmdm  49462  dmdm  50372  infsubc2d  50381