Theorem dmxpid 5911

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 5901	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5664	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5749	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	eqtrdi 2811	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5886	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 23	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2821	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5910	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3038	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

This proof depends on syntax axioms:   = wceq 1569  ∅c0 4278   × cxp 5648  dom cdm 5650

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-xp 5656  df-dm 5660

This theorem is used by:  dmxpin  5912  xpid11  5913  sofld  6178  xpider  8809  hartogslem1  9536  unxpwdom2  9582  infxpenlem  10092  fpwwe2lem12  10727  fpwwe2  10728  canth4  10732  dmrecnq  11053  homfeqbas  17870  sscfn1  17992  sscfn2  17993  ssclem  17994  isssc  17995  rescval2  18003  issubc2  18011  cofuval  18057  resfval2  18068  resf1st  18069  psssdm2  18755  tsrss  18763  decpmatval  23083  pmatcollpw3lem  23101  ustssco  24534  ustbas2  24544  psmetdmdm  24624  xmetdmdm  24654  setsmstopn  24797  tmsval  24800  tngtopn  24969  caufval  25596  grporndm  31112  dfhnorm2  31724  hhshsslem1  31869  metideq  34567  filnetlem4  37211  poimirlem3  38584  ssbnd  38765  bnd2lem  38768  ismtyval  38777  ismndo2  38851  exidreslem  38854  divrngcl  38934  isdrngo2  38935  rtrclex  44660  fnxpdmdm  49300  dmdm  50204  infsubc2d  50213