Theorem rnxp 6160

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

Step	Hyp	Ref	Expression
1		df-rn 5663	. . 3 ⊢ ran (𝐴 × 𝐵) = dom ◡(𝐴 × 𝐵)
2		cnvxp 6146	. . . 4 ⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴)
3	2	dmeqi 5885	. . 3 ⊢ dom ◡(𝐴 × 𝐵) = dom (𝐵 × 𝐴)
4	1, 3	eqtri 2788	. 2 ⊢ ran (𝐴 × 𝐵) = dom (𝐵 × 𝐴)
5		dmxp 5910	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐵 × 𝐴) = 𝐵)
6	4, 5	eqtrid 2812	1 ⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)

Syntax hints:   → wi 4   = wceq 1563   ≠ wne 2960  ∅c0 4288   × cxp 5650  ^◡ccnv 5651  dom cdm 5652  ran crn 5653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-11 2194  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-xp 5658  df-rel 5659  df-cnv 5660  df-dm 5662  df-rn 5663

This theorem is referenced by:  rnxpid  6163  ssxpb  6164  xpima  6172  unixp  6273  fconst5  7194  rnmptc  7195  xpexr  7903  xpexr2  7904  fparlem3  8097  fparlem4  8098  frxp  8110  fodomr  9104  fodomfir  9275  djuexb  9883  dfac5lem3  10097  fpwwe2lem12  10615  vdwlem8  17038  ramz  17075  gsumxp  20037  xkoccn  23737  txindislem  23751  cnextf  24184  metustexhalf  24674  ovolctb  25610  axlowdimlem13  29213  axlowdim1  29218  imadifxp  32856  sibf0  34641  ovoliunnfl  38173  voliunnfl  38175  dmrnxp  49466  idfudiag1lem  50152