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

Theorem dmxpid 5058
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 5052 . . 3  |-  dom  (/)  =  (/)
2 xpeq1 4853 . . . . 5  |-  ( A  =  (/)  ->  ( A  X.  A )  =  ( (/)  X.  A
) )
3 0xp 4916 . . . . 5  |-  ( (/)  X.  A )  =  (/)
42, 3syl6eq 2490 . . . 4  |-  ( A  =  (/)  ->  ( A  X.  A )  =  (/) )
54dmeqd 5041 . . 3  |-  ( A  =  (/)  ->  dom  ( A  X.  A )  =  dom  (/) )
6 id 22 . . 3  |-  ( A  =  (/)  ->  A  =  (/) )
71, 5, 63eqtr4a 2500 . 2  |-  ( A  =  (/)  ->  dom  ( A  X.  A )  =  A )
8 dmxp 5057 . 2  |-  ( A  =/=  (/)  ->  dom  ( A  X.  A )  =  A )
97, 8pm2.61ine 2686 1  |-  dom  ( A  X.  A )  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369   (/)c0 3636    X. cxp 4837   dom cdm 4839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4412  ax-nul 4420  ax-pr 4530
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2719  df-rab 2723  df-v 2973  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-nul 3637  df-if 3791  df-sn 3877  df-pr 3879  df-op 3883  df-br 4292  df-opab 4350  df-xp 4845  df-dm 4849
This theorem is referenced by:  dmxpin  5059  xpid11  5060  sofld  5285  xpider  7170  hartogslem1  7755  unxpwdom2  7802  infxpenlem  8179  fpwwe2lem13  8808  fpwwe2  8809  canth4  8813  dmrecnq  9136  homfeqbas  14634  sscfn1  14729  sscfn2  14730  ssclem  14731  isssc  14732  rescval2  14740  issubc2  14748  cofuval  14791  resfval2  14802  resf1st  14803  psssdm2  15384  tsrss  15392  ustssco  19788  ustbas2  19799  psmetdmdm  19880  xmetdmdm  19909  setsmstopn  20052  tmsval  20055  tngtopn  20235  caufval  20785  grporndm  23696  isabloda  23785  ismndo2  23831  vcoprne  23956  dfhnorm2  24523  hhshsslem1  24667  metideq  26319  filnetlem4  28600  ssbnd  28685  bnd2lem  28688  ismtyval  28697  exidreslem  28740  divrngcl  28761  isdrngo2  28762
  Copyright terms: Public domain W3C validator