Theorem rnxp 6146

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 5652	. . 3 ⊢ ran (𝐴 × 𝐵) = dom ◡(𝐴 × 𝐵)
2		cnvxp 6133	. . . 4 ⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴)
3	2	dmeqi 5871	. . 3 ⊢ dom ◡(𝐴 × 𝐵) = dom (𝐵 × 𝐴)
4	1, 3	eqtri 2753	. 2 ⊢ ran (𝐴 × 𝐵) = dom (𝐵 × 𝐴)
5		dmxp 5895	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐵 × 𝐴) = 𝐵)
6	4, 5	eqtrid 2777	1 ⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2926  ∅c0 4299   × cxp 5639  ^◡ccnv 5640  dom cdm 5641  ran crn 5642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-cnv 5649  df-dm 5651  df-rn 5652

This theorem is referenced by:  rnxpid  6149  ssxpb  6150  xpima  6158  unixp  6258  fconst5  7183  rnmptc  7184  xpexr  7897  xpexr2  7898  fparlem3  8096  fparlem4  8097  frxp  8108  fodomr  9098  fodomfir  9286  djuexb  9869  dfac5lem3  10085  fpwwe2lem12  10602  vdwlem8  16966  ramz  17003  gsumxp  19913  xkoccn  23513  txindislem  23527  cnextf  23960  metustexhalf  24451  ovolctb  25398  axlowdimlem13  28888  axlowdim1  28893  imadifxp  32537  sibf0  34332  ovoliunnfl  37663  voliunnfl  37665  dmrnxp  48829  idfudiag1lem  49516