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

Theorem dmxp 4897
Description: The domain of a cross 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 )
Dummy variables  x  y are mutually distinct and distinct from all other variables.

Proof of Theorem dmxp
StepHypRef Expression
1 df-xp 4695 . . 3  |-  ( A  X.  B )  =  { <. y ,  x >.  |  ( y  e.  A  /\  x  e.  B ) }
21dmeqi 4880 . 2  |-  dom  (  A  X.  B )  =  dom  { <. y ,  x >.  |  (
y  e.  A  /\  x  e.  B ) }
3 n0 3466 . . . . 5  |-  ( B  =/=  (/)  <->  E. x  x  e.  B )
43biimpi 188 . . . 4  |-  ( B  =/=  (/)  ->  E. x  x  e.  B )
54ralrimivw 2629 . . 3  |-  ( B  =/=  (/)  ->  A. y  e.  A  E. x  x  e.  B )
6 dmopab3 4891 . . 3  |-  ( A. y  e.  A  E. x  x  e.  B  <->  dom 
{ <. y ,  x >.  |  ( y  e.  A  /\  x  e.  B ) }  =  A )
75, 6sylib 190 . 2  |-  ( B  =/=  (/)  ->  dom  { <. y ,  x >.  |  ( y  e.  A  /\  x  e.  B ) }  =  A )
82, 7syl5eq 2329 1  |-  ( B  =/=  (/)  ->  dom  (  A  X.  B )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360   E.wex 1529    = wceq 1624    e. wcel 1685    =/= wne 2448   A.wral 2545   (/)c0 3457   {copab 4078    X. cxp 4687   dom cdm 4689
This theorem is referenced by:  dmxpid  4898  rnxp  5106  dmxpss  5107  ssxpb  5110  xpexr2  5115  relrelss  5195  unixp  5204  frxp  6187  fodomr  7008  nqerf  8550  pwsbas  13381  pwsle  13386  imasaddfnlem  13425  imasvscafn  13434  efgrcl  15019  txindislem  17322  dveq0  19342  dv11cn  19343  ismgm  20980  axbday  23730  axfelem3  23750  prjcp1  24483  cur1vald  24599  valcurfn1  24604  rngmgmbs3  24817  diophrw  26238  xpexcnv  27059
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4214
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026  df-opab 4080  df-xp 4695  df-dm 4699
  Copyright terms: Public domain W3C validator