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

Theorem dmxp 5041
Description: The domain of a Cartesian product. Part of Theorem 3.13(x) of [Monk1] p. 37. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
dmxp  |-  ( B  =/=  (/)  ->  dom  ( A  X.  B )  =  A )

Proof of Theorem dmxp
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-xp 4828 . . 3  |-  ( A  X.  B )  =  { <. y ,  x >.  |  ( y  e.  A  /\  x  e.  B ) }
21dmeqi 5024 . 2  |-  dom  ( A  X.  B )  =  dom  { <. y ,  x >.  |  (
y  e.  A  /\  x  e.  B ) }
3 n0 3747 . . . . 5  |-  ( B  =/=  (/)  <->  E. x  x  e.  B )
43biimpi 194 . . . 4  |-  ( B  =/=  (/)  ->  E. x  x  e.  B )
54ralrimivw 2818 . . 3  |-  ( B  =/=  (/)  ->  A. y  e.  A  E. x  x  e.  B )
6 dmopab3 5035 . . 3  |-  ( A. y  e.  A  E. x  x  e.  B  <->  dom 
{ <. y ,  x >.  |  ( y  e.  A  /\  x  e.  B ) }  =  A )
75, 6sylib 196 . 2  |-  ( B  =/=  (/)  ->  dom  { <. y ,  x >.  |  ( y  e.  A  /\  x  e.  B ) }  =  A )
82, 7syl5eq 2455 1  |-  ( B  =/=  (/)  ->  dom  ( A  X.  B )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1405   E.wex 1633    e. wcel 1842    =/= wne 2598   A.wral 2753   (/)c0 3737   {copab 4451    X. cxp 4820   dom cdm 4822
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395  df-opab 4453  df-xp 4828  df-dm 4832
This theorem is referenced by:  dmxpid  5042  rnxp  5254  dmxpss  5255  ssxpb  5258  relrelss  5346  unixp  5356  xpexr2  6724  xpexcnv  6725  frxp  6893  mpt2curryd  7000  fodomr  7705  nqerf  9337  dmtrclfv  12999  pwsbas  15099  pwsle  15104  imasaddfnlem  15140  imasvscafn  15149  efgrcl  17055  frlmip  19103  txindislem  20424  metustexhalfOLD  21356  metustexhalf  21357  rrxip  22112  dveq0  22691  dv11cn  22692  ismgmOLD  25722  mbfmcst  28693  eulerpartlemt  28802  0rrv  28882  bdayfo  30122  nobndlem3  30141  diophrw  35033
  Copyright terms: Public domain W3C validator