MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmxpid Structured version   Visualization version   GIF version

Theorem dmxpid 5377
Description: The domain of a square Cartesian product. (Contributed by NM, 28-Jul-1995.)
Assertion
Ref Expression
dmxpid dom (𝐴 × 𝐴) = 𝐴

Proof of Theorem dmxpid
StepHypRef Expression
1 dm0 5371 . . 3 dom ∅ = ∅
2 xpeq1 5157 . . . . 5 (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3 0xp 5233 . . . . 5 (∅ × 𝐴) = ∅
42, 3syl6eq 2701 . . . 4 (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
54dmeqd 5358 . . 3 (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6 id 22 . . 3 (𝐴 = ∅ → 𝐴 = ∅)
71, 5, 63eqtr4a 2711 . 2 (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8 dmxp 5376 . 2 (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
97, 8pm2.61ine 2906 1 dom (𝐴 × 𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  c0 3948   × cxp 5141  dom cdm 5143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-xp 5149  df-dm 5153
This theorem is referenced by:  dmxpin  5378  xpid11  5379  sofld  5616  xpider  7861  hartogslem1  8488  unxpwdom2  8534  infxpenlem  8874  fpwwe2lem13  9502  fpwwe2  9503  canth4  9507  dmrecnq  9828  homfeqbas  16403  sscfn1  16524  sscfn2  16525  ssclem  16526  isssc  16527  rescval2  16535  issubc2  16543  cofuval  16589  resfval2  16600  resf1st  16601  psssdm2  17262  tsrss  17270  decpmatval  20618  pmatcollpw3lem  20636  ustssco  22065  ustbas2  22076  psmetdmdm  22157  xmetdmdm  22187  setsmstopn  22330  tmsval  22333  tngtopn  22501  caufval  23119  grporndm  27492  dfhnorm2  28107  hhshsslem1  28252  metideq  30064  filnetlem4  32501  poimirlem3  33542  ssbnd  33717  bnd2lem  33720  ismtyval  33729  ismndo2  33803  exidreslem  33806  divrngcl  33886  isdrngo2  33887  rtrclex  38241  fnxpdmdm  42093
  Copyright terms: Public domain W3C validator