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

Theorem rnxp 6122
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 (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)

Proof of Theorem rnxp
StepHypRef Expression
1 df-rn 5644 . . 3 ran (𝐴 × 𝐵) = dom (𝐴 × 𝐵)
2 cnvxp 6109 . . . 4 (𝐴 × 𝐵) = (𝐵 × 𝐴)
32dmeqi 5860 . . 3 dom (𝐴 × 𝐵) = dom (𝐵 × 𝐴)
41, 3eqtri 2764 . 2 ran (𝐴 × 𝐵) = dom (𝐵 × 𝐴)
5 dmxp 5884 . 2 (𝐴 ≠ ∅ → dom (𝐵 × 𝐴) = 𝐵)
64, 5eqtrid 2788 1 (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wne 2943  c0 4282   × cxp 5631  ccnv 5632  dom cdm 5633  ran crn 5634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-br 5106  df-opab 5168  df-xp 5639  df-rel 5640  df-cnv 5641  df-dm 5643  df-rn 5644
This theorem is referenced by:  rnxpid  6125  ssxpb  6126  xpima  6134  unixp  6234  fconst5  7155  rnmptc  7156  xpexr  7855  xpexr2  7856  fparlem3  8046  fparlem4  8047  frxp  8058  fodomr  9072  djuexb  9845  dfac5lem3  10061  fpwwe2lem12  10578  vdwlem8  16860  ramz  16897  gsumxp  19753  xkoccn  22970  txindislem  22984  cnextf  23417  metustexhalf  23912  ovolctb  24854  axlowdimlem13  27903  axlowdim1  27908  imadifxp  31519  sibf0  32934  ovoliunnfl  36120  voliunnfl  36122
  Copyright terms: Public domain W3C validator