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

Theorem rnxp 5424
Description: The range of a Cartesian product. Part of Theorem 3.13(x) of [Monk1] p. 37. (Contributed by NM, 12-Apr-2004.)
Assertion
Ref Expression
rnxp  |-  ( A  =/=  (/)  ->  ran  ( A  X.  B )  =  B )

Proof of Theorem rnxp
StepHypRef Expression
1 df-rn 4997 . . 3  |-  ran  ( A  X.  B )  =  dom  `' ( A  X.  B )
2 cnvxp 5411 . . . 4  |-  `' ( A  X.  B )  =  ( B  X.  A )
32dmeqi 5191 . . 3  |-  dom  `' ( A  X.  B
)  =  dom  ( B  X.  A )
41, 3eqtri 2470 . 2  |-  ran  ( A  X.  B )  =  dom  ( B  X.  A )
5 dmxp 5208 . 2  |-  ( A  =/=  (/)  ->  dom  ( B  X.  A )  =  B )
64, 5syl5eq 2494 1  |-  ( A  =/=  (/)  ->  ran  ( A  X.  B )  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1381    =/= wne 2636   (/)c0 3768    X. cxp 4984   `'ccnv 4985   dom cdm 4986   ran crn 4987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pr 4673
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-br 4435  df-opab 4493  df-xp 4992  df-rel 4993  df-cnv 4994  df-dm 4996  df-rn 4997
This theorem is referenced by:  rnxpid  5427  ssxpb  5428  xpima  5436  unixp  5527  fconst5  6110  xpexr  6722  xpexr2  6723  fparlem3  6884  fparlem4  6885  frxp  6892  fodomr  7667  dfac5lem3  8506  fpwwe2lem13  9020  vdwlem8  14380  ramz  14417  gsumxp  16875  gsumxpOLD  16877  xkoccn  19990  txindislem  20004  cnextf  20436  metustexhalfOLD  20936  metustexhalf  20937  ovolctb  21771  axlowdimlem13  24126  axlowdim1  24131  imadifxp  27327  sibf0  28146  ovoliunnfl  30028  voliunnfl  30030
  Copyright terms: Public domain W3C validator