Theorem dmxpid 5227

Description: The domain of a square Cartesian product. (Contributed by NM, 28-Jul-1995.)

Assertion

Ref	Expression
dmxpid

Proof of Theorem dmxpid

Step	Hyp	Ref	Expression
1		dm0 5221	. . 3
2		xpeq1 5018	. . . . 5
3		0xp 5085	. . . . 5
4	2, 3	syl6eq 2514	. . . 4
5	4	dmeqd 5210	. . 3
6		id 22	. . 3
7	1, 5, 6	3eqtr4a 2524	. 2
8		dmxp 5226	. 2
9	7, 8	pm2.61ine 2770	1

Syntax hints:  =wceq 1395  c0 3784  X.cxp 5002  domcdm 5004

This theorem is referenced by:  dmxpin  5228  xpid11  5229  sofld  5460  xpider  7401  hartogslem1  7988  unxpwdom2  8035  infxpenlem  8412  fpwwe2lem13  9041  fpwwe2  9042  canth4  9046  dmrecnq  9367  homfeqbas  15091  sscfn1  15186  sscfn2  15187  ssclem  15188  isssc  15189  rescval2  15197  issubc2  15205  cofuval  15251  resfval2  15262  resf1st  15263  psssdm2  15845  tsrss  15853  decpmatval  19266  pmatcollpw3lem  19284  ustssco  20717  ustbas2  20728  psmetdmdm  20809  xmetdmdm  20838  setsmstopn  20981  tmsval  20984  tngtopn  21164  caufval  21714  grporndm  25212  isabloda  25301  ismndo2  25347  vcoprne  25472  dfhnorm2  26039  hhshsslem1  26183  metideq  27872  filnetlem4  30199  ssbnd  30284  bnd2lem  30287  ismtyval  30296  exidreslem  30339  divrngcl  30360  isdrngo2  30361  fnxpdmdm  32456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010  df-dm 5014