Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rnxp | Structured version Visualization version GIF version |
Description: The range of a Cartesian product. Part of Theorem 3.13(x) of [Monk1] p. 37. (Contributed by NM, 12-Apr-2004.) |
Ref | Expression |
---|---|
rnxp | ⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵) |
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 (𝐴 × 𝐵) = 𝐵) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |