Theorem dmxpid 5345

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

Step	Hyp	Ref	Expression
1		dm0 5339	. . 3 |- dom (/) = (/)
2		xpeq1 5128	. . . . 5 |- ( A = (/) -> ( A X. A ) = ( (/) X. A ) )
3		0xp 5199	. . . . 5 |- ( (/) X. A ) = (/)
4	2, 3	syl6eq 2672	. . . 4 |- ( A = (/) -> ( A X. A ) = (/) )
5	4	dmeqd 5326	. . 3 |- ( A = (/) -> dom ( A X. A ) = dom (/) )
6		id 22	. . 3 |- ( A = (/) -> A = (/) )
7	1, 5, 6	3eqtr4a 2682	. 2 |- ( A = (/) -> dom ( A X. A ) = A )
8		dmxp 5344	. 2 |- ( A =/= (/) -> dom ( A X. A ) = A )
9	7, 8	pm2.61ine 2877	1 |- dom ( A X. A ) = A

Syntax hints:   = wceq 1483   (/)c0 3915   X. cxp 5112   dom cdm 5114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-dm 5124

This theorem is referenced by:  dmxpin  5346  xpid11  5347  sofld  5581  xpider  7818  hartogslem1  8447  unxpwdom2  8493  infxpenlem  8836  fpwwe2lem13  9464  fpwwe2  9465  canth4  9469  dmrecnq  9790  homfeqbas  16356  sscfn1  16477  sscfn2  16478  ssclem  16479  isssc  16480  rescval2  16488  issubc2  16496  cofuval  16542  resfval2  16553  resf1st  16554  psssdm2  17215  tsrss  17223  decpmatval  20570  pmatcollpw3lem  20588  ustssco  22018  ustbas2  22029  psmetdmdm  22110  xmetdmdm  22140  setsmstopn  22283  tmsval  22286  tngtopn  22454  caufval  23073  grporndm  27364  dfhnorm2  27979  hhshsslem1  28124  metideq  29936  filnetlem4  32376  poimirlem3  33412  ssbnd  33587  bnd2lem  33590  ismtyval  33599  ismndo2  33673  exidreslem  33676  divrngcl  33756  isdrngo2  33757  rtrclex  37924  fnxpdmdm  41768