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

Step	Hyp	Ref	Expression
1		df-rn 5630	. . 3 ⊢ ran (𝐴 × 𝐵) = dom ◡(𝐴 × 𝐵)
2		cnvxp 6109	. . . 4 ⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴)
3	2	dmeqi 5848	. . 3 ⊢ dom ◡(𝐴 × 𝐵) = dom (𝐵 × 𝐴)
4	1, 3	eqtri 2756	. 2 ⊢ ran (𝐴 × 𝐵) = dom (𝐵 × 𝐴)
5		dmxp 5873	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐵 × 𝐴) = 𝐵)
6	4, 5	eqtrid 2780	1 ⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2929  ∅c0 4282   × cxp 5617  ^◡ccnv 5618  dom cdm 5619  ran crn 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-11 2162  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-xp 5625  df-rel 5626  df-cnv 5627  df-dm 5629  df-rn 5630

This theorem is referenced by:  rnxpid  6125  ssxpb  6126  xpima  6134  unixp  6234  fconst5  7146  rnmptc  7147  xpexr  7854  xpexr2  7855  fparlem3  8050  fparlem4  8051  frxp  8062  fodomr  9048  fodomfir  9219  djuexb  9809  dfac5lem3  10023  fpwwe2lem12  10540  vdwlem8  16902  ramz  16939  gsumxp  19890  xkoccn  23535  txindislem  23549  cnextf  23982  metustexhalf  24472  ovolctb  25419  axlowdimlem13  28934  axlowdim1  28939  imadifxp  32583  sibf0  34368  ovoliunnfl  37722  voliunnfl  37724  dmrnxp  48961  idfudiag1lem  49648