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

Theorem dmxpid 5500
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 5494 . . 3 dom ∅ = ∅
2 xpeq1 5280 . . . . 5 (𝐴 = ∅ → (𝐴 × 𝐴) = (∅ × 𝐴))
3 0xp 5356 . . . . 5 (∅ × 𝐴) = ∅
42, 3syl6eq 2810 . . . 4 (𝐴 = ∅ → (𝐴 × 𝐴) = ∅)
54dmeqd 5481 . . 3 (𝐴 = ∅ → dom (𝐴 × 𝐴) = dom ∅)
6 id 22 . . 3 (𝐴 = ∅ → 𝐴 = ∅)
71, 5, 63eqtr4a 2820 . 2 (𝐴 = ∅ → dom (𝐴 × 𝐴) = 𝐴)
8 dmxp 5499 . 2 (𝐴 ≠ ∅ → dom (𝐴 × 𝐴) = 𝐴)
97, 8pm2.61ine 3015 1 dom (𝐴 × 𝐴) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  c0 4058   × cxp 5264  dom cdm 5266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-xp 5272  df-dm 5276
This theorem is referenced by:  dmxpin  5501  xpid11  5502  sofld  5739  xpider  7985  hartogslem1  8612  unxpwdom2  8658  infxpenlem  9026  fpwwe2lem13  9656  fpwwe2  9657  canth4  9661  dmrecnq  9982  homfeqbas  16557  sscfn1  16678  sscfn2  16679  ssclem  16680  isssc  16681  rescval2  16689  issubc2  16697  cofuval  16743  resfval2  16754  resf1st  16755  psssdm2  17416  tsrss  17424  decpmatval  20772  pmatcollpw3lem  20790  ustssco  22219  ustbas2  22230  psmetdmdm  22311  xmetdmdm  22341  setsmstopn  22484  tmsval  22487  tngtopn  22655  caufval  23273  grporndm  27673  dfhnorm2  28288  hhshsslem1  28433  metideq  30245  filnetlem4  32682  poimirlem3  33725  ssbnd  33900  bnd2lem  33903  ismtyval  33912  ismndo2  33986  exidreslem  33989  divrngcl  34069  isdrngo2  34070  rtrclex  38426  fnxpdmdm  42278
  Copyright terms: Public domain W3C validator