Theorem dmxpid 3333

Description: The domain of a square cross product.

Assertion

Ref	Expression
dmxpid	|- dom ( A X. A) = A

Proof of Theorem dmxpid

Step	Hyp	Ref	Expression
1		dm0 3323	. . 3 |- dom (/) = (/)
2		xpeq1 3200	. . . . 5 |- (A = (/) -> (A X. A) = ((/) X. A))
3		xp0r 3239	. . . . 5 |- ((/) X. A) = (/)
4	2, 3	syl6eq 1523	. . . 4 |- (A = (/) -> (A X. A) = (/))
5	4	dmeqd 3313	. . 3 |- (A = (/) -> dom ( A X. A) = dom (/))
6		id 59	. . 3 |- (A = (/) -> A = (/))
7	1, 5, 6	3eqtr4a 1532	. 2 |- (A = (/) -> dom ( A X. A) = A)
8		dmxp 3332	. 2 |- (A =/= (/) -> dom ( A X. A) = A)
9	7, 8	pm2.61ine 1634	1 |- dom ( A X. A) = A

Syntax hints:   = wceq 956  (/)c0 2280   X. cxp 3168  dom cdm 3170

This theorem is referenced by:  dmxpin 3334  xpid11 3335  ecopoprdm 4309  ismet 7798  dfms2 7799  ismeti 7802  metreslem 7822  cnmetba 7903  cncfmet 7905  remetba 7909  xplmi 7973  xplmi2 7974  xplm 7975  xpcn 7976  oprcn 7977  bopcnlem3 7983  bopcn 7985  grprndm 8054  vcoprne 8198  imsba 8321  dfhnorm2 8988  hhshsslem1 9137  dmhmph 10532  reldded 10674  reldcat 10695

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620  df-opab 2667  df-xp 3184  df-dm 3188

Copyright terms: Public domain