Theorem rnxp 6000

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 5536	. . 3 ⊢ ran (𝐴 × 𝐵) = dom ◡(𝐴 × 𝐵)
2		cnvxp 5987	. . . 4 ⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴)
3	2	dmeqi 5745	. . 3 ⊢ dom ◡(𝐴 × 𝐵) = dom (𝐵 × 𝐴)
4	1, 3	eqtri 2782	. 2 ⊢ ran (𝐴 × 𝐵) = dom (𝐵 × 𝐴)
5		dmxp 5771	. 2 ⊢ (𝐴 ≠ ∅ → dom (𝐵 × 𝐴) = 𝐵)
6	4, 5	syl5eq 2806	1 ⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵)

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2952  ∅c0 4226   × cxp 5523  ^◡ccnv 5524  dom cdm 5525  ran crn 5526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pr 5299

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-v 3412  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-sn 4524  df-pr 4526  df-op 4530  df-br 5034  df-opab 5096  df-xp 5531  df-rel 5532  df-cnv 5533  df-dm 5535  df-rn 5536

This theorem is referenced by:  rnxpid  6003  ssxpb  6004  xpima  6012  unixp  6112  fconst5  6960  rnmptc  6961  xpexr  7629  xpexr2  7630  fparlem3  7815  fparlem4  7816  frxp  7826  fodomr  8690  djuexb  9364  dfac5lem3  9578  fpwwe2lem12  10095  vdwlem8  16372  ramz  16409  gsumxp  19157  xkoccn  22312  txindislem  22326  cnextf  22759  metustexhalf  23251  ovolctb  24183  axlowdimlem13  26840  axlowdim1  26845  imadifxp  30455  sibf0  31813  ovoliunnfl  35372  voliunnfl  35374