Theorem rnxp 6013

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 5552	. . 3 ⊢ ran (𝐴 × 𝐵) = dom ◡(𝐴 × 𝐵)
2		cnvxp 6000	. . . 4 ⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴)
3	2	dmeqi 5759	. . 3 ⊢ dom ◡(𝐴 × 𝐵) = dom (𝐵 × 𝐴)
4	1, 3	eqtri 2844	. 2 ⊢ ran (𝐴 × 𝐵) = dom (𝐵 × 𝐴)
5		dmxp 5785	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐵 × 𝐴) = 𝐵)
6	4, 5	syl5eq 2868	1 ⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 3016  ∅c0 4279   × cxp 5539  ^◡ccnv 5540  dom cdm 5541  ran crn 5542

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5189  ax-nul 5196  ax-pr 5316

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rab 3147  df-v 3488  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-sn 4554  df-pr 4556  df-op 4560  df-br 5053  df-opab 5115  df-xp 5547  df-rel 5548  df-cnv 5549  df-dm 5551  df-rn 5552

This theorem is referenced by:  rnxpid  6016  ssxpb  6017  xpima  6025  unixp  6119  fconst5  6954  rnmptc  6955  xpexr  7609  xpexr2  7610  fparlem3  7795  fparlem4  7796  frxp  7806  fodomr  8654  djuexb  9324  dfac5lem3  9537  fpwwe2lem13  10050  vdwlem8  16307  ramz  16344  gsumxp  19079  xkoccn  22210  txindislem  22224  cnextf  22657  metustexhalf  23149  ovolctb  24074  axlowdimlem13  26726  axlowdim1  26731  imadifxp  30337  sibf0  31599  ovoliunnfl  34968  voliunnfl  34970