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

Theorem dmxpid 4898
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 4892 . . 3  |-  dom  (/)  =  (/)
2 xpeq1 4703 . . . . 5  |-  ( A  =  (/)  ->  ( A  X.  A )  =  ( (/)  X.  A
) )
3 xp0r 4768 . . . . 5  |-  ( (/)  X.  A )  =  (/)
42, 3syl6eq 2331 . . . 4  |-  ( A  =  (/)  ->  ( A  X.  A )  =  (/) )
54dmeqd 4881 . . 3  |-  ( A  =  (/)  ->  dom  ( A  X.  A )  =  dom  (/) )
6 id 19 . . 3  |-  ( A  =  (/)  ->  A  =  (/) )
71, 5, 63eqtr4a 2341 . 2  |-  ( A  =  (/)  ->  dom  ( A  X.  A )  =  A )
8 dmxp 4897 . 2  |-  ( A  =/=  (/)  ->  dom  ( A  X.  A )  =  A )
97, 8pm2.61ine 2522 1  |-  dom  ( A  X.  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1623   (/)c0 3455    X. cxp 4687   dom cdm 4689
This theorem is referenced by:  dmxpin  4899  xpid11  4900  sofld  5121  xpider  6730  hartogslem1  7257  unxpwdom2  7302  infxpenlem  7641  fpwwe2lem13  8264  fpwwe2  8265  canth4  8269  dmrecnq  8592  homfeqbas  13599  sscfn1  13694  sscfn2  13695  ssclem  13696  isssc  13697  rescval2  13705  issubc2  13713  cofuval  13756  resfval2  13767  resf1st  13768  psssdm2  14324  tsrss  14332  xmetdmdm  17900  setsmstopn  18024  tmsval  18027  tngtopn  18166  caufval  18701  grporndm  20877  isabloda  20966  ismndo2  21012  vcoprne  21135  dfhnorm2  21701  hhshsslem1  21844  nZdef  25180  islatalg  25183  rngodmeqrn  25419  zintdom  25438  svs2  25487  reldded  25741  reldcat  25762  filnetlem4  26330  ssbnd  26512  bnd2lem  26515  ismtyval  26524  exidreslem  26567  divrngcl  26588  isdrngo2  26589
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-xp 4695  df-dm 4699
  Copyright terms: Public domain W3C validator