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

Theorem dmxpid 5089
Description: The domain of a square cross product. (Contributed by NM, 28-Jul-1995.)
Assertion
Ref Expression
dmxpid  |-  dom  ( A  X.  A )  =  A

Proof of Theorem dmxpid
StepHypRef Expression
1 dm0 5083 . . 3  |-  dom  (/)  =  (/)
2 xpeq1 4892 . . . . 5  |-  ( A  =  (/)  ->  ( A  X.  A )  =  ( (/)  X.  A
) )
3 xp0r 4956 . . . . 5  |-  ( (/)  X.  A )  =  (/)
42, 3syl6eq 2484 . . . 4  |-  ( A  =  (/)  ->  ( A  X.  A )  =  (/) )
54dmeqd 5072 . . 3  |-  ( A  =  (/)  ->  dom  ( A  X.  A )  =  dom  (/) )
6 id 20 . . 3  |-  ( A  =  (/)  ->  A  =  (/) )
71, 5, 63eqtr4a 2494 . 2  |-  ( A  =  (/)  ->  dom  ( A  X.  A )  =  A )
8 dmxp 5088 . 2  |-  ( A  =/=  (/)  ->  dom  ( A  X.  A )  =  A )
97, 8pm2.61ine 2680 1  |-  dom  ( A  X.  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1652   (/)c0 3628    X. cxp 4876   dom cdm 4878
This theorem is referenced by:  dmxpin  5090  xpid11  5091  sofld  5318  xpider  6975  hartogslem1  7511  unxpwdom2  7556  infxpenlem  7895  fpwwe2lem13  8517  fpwwe2  8518  canth4  8522  dmrecnq  8845  homfeqbas  13922  sscfn1  14017  sscfn2  14018  ssclem  14019  isssc  14020  rescval2  14028  issubc2  14036  cofuval  14079  resfval2  14090  resf1st  14091  psssdm2  14647  tsrss  14655  ustssco  18244  ustbas2  18255  psmetdmdm  18336  xmetdmdm  18365  setsmstopn  18508  tmsval  18511  tngtopn  18691  caufval  19228  grporndm  21798  isabloda  21887  ismndo2  21933  vcoprne  22058  dfhnorm2  22624  hhshsslem1  22767  metideq  24288  filnetlem4  26410  ssbnd  26497  bnd2lem  26500  ismtyval  26509  exidreslem  26552  divrngcl  26573  isdrngo2  26574
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pr 4403
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213  df-opab 4267  df-xp 4884  df-dm 4888
  Copyright terms: Public domain W3C validator