Theorem rnxp 6128

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 5635	. . 3 ⊢ ran (𝐴 × 𝐵) = dom ◡(𝐴 × 𝐵)
2		cnvxp 6115	. . . 4 ⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴)
3	2	dmeqi 5853	. . 3 ⊢ dom ◡(𝐴 × 𝐵) = dom (𝐵 × 𝐴)
4	1, 3	eqtri 2760	. 2 ⊢ ran (𝐴 × 𝐵) = dom (𝐵 × 𝐴)
5		dmxp 5878	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐵 × 𝐴) = 𝐵)
6	4, 5	eqtrid 2784	1 ⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2933  ∅c0 4274   × cxp 5622  ^◡ccnv 5623  dom cdm 5624  ran crn 5625

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-11 2163  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630  df-rel 5631  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  rnxpid  6131  ssxpb  6132  xpima  6140  unixp  6240  fconst5  7154  rnmptc  7155  xpexr  7862  xpexr2  7863  fparlem3  8057  fparlem4  8058  frxp  8069  fodomr  9059  fodomfir  9231  djuexb  9824  dfac5lem3  10038  fpwwe2lem12  10556  vdwlem8  16950  ramz  16987  gsumxp  19942  xkoccn  23594  txindislem  23608  cnextf  24041  metustexhalf  24531  ovolctb  25467  axlowdimlem13  29037  axlowdim1  29042  imadifxp  32686  sibf0  34494  ovoliunnfl  37997  voliunnfl  37999  dmrnxp  49324  idfudiag1lem  50010