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

Theorem dmxp 5227
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 5011 . . 3  |-  ( A  X.  B )  =  { <. y ,  x >.  |  ( y  e.  A  /\  x  e.  B ) }
21dmeqi 5210 . 2  |-  dom  ( A  X.  B )  =  dom  { <. y ,  x >.  |  (
y  e.  A  /\  x  e.  B ) }
3 n0 3799 . . . . 5  |-  ( B  =/=  (/)  <->  E. x  x  e.  B )
43biimpi 194 . . . 4  |-  ( B  =/=  (/)  ->  E. x  x  e.  B )
54ralrimivw 2882 . . 3  |-  ( B  =/=  (/)  ->  A. y  e.  A  E. x  x  e.  B )
6 dmopab3 5221 . . 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 2520 1  |-  ( B  =/=  (/)  ->  dom  ( A  X.  B )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379   E.wex 1596    e. wcel 1767    =/= wne 2662   A.wral 2817   (/)c0 3790   {copab 4510    X. cxp 5003   dom cdm 5005
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pr 4692
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rab 2826  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-br 4454  df-opab 4512  df-xp 5011  df-dm 5015
This theorem is referenced by:  dmxpid  5228  rnxp  5443  dmxpss  5444  ssxpb  5447  relrelss  5537  unixp  5546  xpexr2  6736  xpexcnv  6737  frxp  6905  mpt2curryd  7010  fodomr  7680  nqerf  9320  pwsbas  14759  pwsle  14764  imasaddfnlem  14800  imasvscafn  14809  efgrcl  16606  frlmip  18678  txindislem  20002  metustexhalfOLD  20934  metustexhalf  20935  rrxip  21690  dveq0  22269  dv11cn  22270  ismgmOLD  25145  mbfmcst  28055  eulerpartlemt  28135  0rrv  28215  bdayfo  29362  nobndlem3  29381  diophrw  30620
  Copyright terms: Public domain W3C validator