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

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

Proof of Theorem dmxpid
StepHypRef Expression
1 dm0 5205 . . 3  |-  dom  (/)  =  (/)
2 xpeq1 5002 . . . . 5  |-  ( A  =  (/)  ->  ( A  X.  A )  =  ( (/)  X.  A
) )
3 0xp 5069 . . . . 5  |-  ( (/)  X.  A )  =  (/)
42, 3syl6eq 2511 . . . 4  |-  ( A  =  (/)  ->  ( A  X.  A )  =  (/) )
54dmeqd 5194 . . 3  |-  ( A  =  (/)  ->  dom  ( A  X.  A )  =  dom  (/) )
6 id 22 . . 3  |-  ( A  =  (/)  ->  A  =  (/) )
71, 5, 63eqtr4a 2521 . 2  |-  ( A  =  (/)  ->  dom  ( A  X.  A )  =  A )
8 dmxp 5210 . 2  |-  ( A  =/=  (/)  ->  dom  ( A  X.  A )  =  A )
97, 8pm2.61ine 2767 1  |-  dom  ( A  X.  A )  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398   (/)c0 3783    X. cxp 4986   dom cdm 4988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498  df-xp 4994  df-dm 4998
This theorem is referenced by:  dmxpin  5212  xpid11  5213  sofld  5439  xpider  7374  hartogslem1  7959  unxpwdom2  8006  infxpenlem  8382  fpwwe2lem13  9009  fpwwe2  9010  canth4  9014  dmrecnq  9335  homfeqbas  15187  sscfn1  15308  sscfn2  15309  ssclem  15310  isssc  15311  rescval2  15319  issubc2  15327  cofuval  15373  resfval2  15384  resf1st  15385  psssdm2  16047  tsrss  16055  decpmatval  19436  pmatcollpw3lem  19454  ustssco  20886  ustbas2  20897  psmetdmdm  20978  xmetdmdm  21007  setsmstopn  21150  tmsval  21153  tngtopn  21333  caufval  21883  grporndm  25413  isabloda  25502  ismndo2  25548  vcoprne  25673  dfhnorm2  26240  hhshsslem1  26384  metideq  28110  filnetlem4  30442  ssbnd  30527  bnd2lem  30530  ismtyval  30539  exidreslem  30582  divrngcl  30603  isdrngo2  30604  fnxpdmdm  32847
  Copyright terms: Public domain W3C validator