Theorem dmxpid 5800

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 5790	. . 3 ⊢ dom ∅ = ∅
2		xpeq1 5569	. . . . 5 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3		0xp 5649	. . . . 5 ⊢ (∅ × 𝐴) = ∅
4	2, 3	syl6eq 2872	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
5	4	dmeqd 5774	. . 3 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6		id 22	. . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∅)
7	1, 5, 6	3eqtr4a 2882	. 2 ⊢ (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8		dmxp 5799	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
9	7, 8	pm2.61ine 3100	1 ⊢ dom (𝐴 × 𝐴) = 𝐴

Syntax hints:   = wceq 1537  ∅c0 4291   × cxp 5553  dom cdm 5555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-dm 5565

This theorem is referenced by:  dmxpin  5801  xpid11  5802  sofld  6044  xpider  8368  hartogslem1  9006  unxpwdom2  9052  infxpenlem  9439  fpwwe2lem13  10064  fpwwe2  10065  canth4  10069  dmrecnq  10390  homfeqbas  16966  sscfn1  17087  sscfn2  17088  ssclem  17089  isssc  17090  rescval2  17098  issubc2  17106  cofuval  17152  resfval2  17163  resf1st  17164  psssdm2  17825  tsrss  17833  decpmatval  21373  pmatcollpw3lem  21391  ustssco  22823  ustbas2  22834  psmetdmdm  22915  xmetdmdm  22945  setsmstopn  23088  tmsval  23091  tngtopn  23259  caufval  23878  grporndm  28287  dfhnorm2  28899  hhshsslem1  29044  metideq  31133  filnetlem4  33729  poimirlem3  34910  ssbnd  35081  bnd2lem  35084  ismtyval  35093  ismndo2  35167  exidreslem  35170  divrngcl  35250  isdrngo2  35251  rtrclex  39997  fnxpdmdm  44055