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

Theorem dmxp 5072
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 4859 . . 3  |-  ( A  X.  B )  =  { <. y ,  x >.  |  ( y  e.  A  /\  x  e.  B ) }
21dmeqi 5055 . 2  |-  dom  ( A  X.  B )  =  dom  { <. y ,  x >.  |  (
y  e.  A  /\  x  e.  B ) }
3 n0 3771 . . . . 5  |-  ( B  =/=  (/)  <->  E. x  x  e.  B )
43biimpi 197 . . . 4  |-  ( B  =/=  (/)  ->  E. x  x  e.  B )
54ralrimivw 2837 . . 3  |-  ( B  =/=  (/)  ->  A. y  e.  A  E. x  x  e.  B )
6 dmopab3 5066 . . 3  |-  ( A. y  e.  A  E. x  x  e.  B  <->  dom 
{ <. y ,  x >.  |  ( y  e.  A  /\  x  e.  B ) }  =  A )
75, 6sylib 199 . 2  |-  ( B  =/=  (/)  ->  dom  { <. y ,  x >.  |  ( y  e.  A  /\  x  e.  B ) }  =  A )
82, 7syl5eq 2475 1  |-  ( B  =/=  (/)  ->  dom  ( A  X.  B )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437   E.wex 1657    e. wcel 1872    =/= wne 2614   A.wral 2771   (/)c0 3761   {copab 4481    X. cxp 4851   dom cdm 4853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-xp 4859  df-dm 4863
This theorem is referenced by:  dmxpid  5073  rnxp  5286  dmxpss  5287  ssxpb  5290  relrelss  5378  unixp  5388  xpexr2  6748  xpexcnv  6749  frxp  6917  mpt2curryd  7027  fodomr  7732  nqerf  9362  dmtrclfv  13082  pwsbas  15384  pwsle  15389  imasaddfnlem  15433  imasvscafn  15442  efgrcl  17364  frlmip  19334  txindislem  20646  metustexhalf  21569  rrxip  22347  dveq0  22950  dv11cn  22951  ismgmOLD  26046  mbfmcst  29089  eulerpartlemt  29212  0rrv  29292  bdayfo  30569  nobndlem3  30588  diophrw  35570
  Copyright terms: Public domain W3C validator