![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fniunfv | Structured version Visualization version GIF version |
Description: The indexed union of a function's values is the union of its range. Compare Definition 5.4 of [Monk1] p. 50. (Contributed by NM, 27-Sep-2004.) |
Ref | Expression |
---|---|
fniunfv | ⊢ (𝐹 Fn 𝐴 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ ran 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvex 6855 | . . 3 ⊢ (𝐹‘𝑥) ∈ V | |
2 | 1 | dfiun2 4993 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} |
3 | fnrnfv 6902 | . . 3 ⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}) | |
4 | 3 | unieqd 4879 | . 2 ⊢ (𝐹 Fn 𝐴 → ∪ ran 𝐹 = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}) |
5 | 2, 4 | eqtr4id 2795 | 1 ⊢ (𝐹 Fn 𝐴 → ∪ 𝑥 ∈ 𝐴 (𝐹‘𝑥) = ∪ ran 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 {cab 2713 ∃wrex 3073 ∪ cuni 4865 ∪ ciun 4954 ran crn 5634 Fn wfn 6491 ‘cfv 6496 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-iota 6448 df-fun 6498 df-fn 6499 df-fv 6504 |
This theorem is referenced by: funiunfv 7194 dffi3 9366 jech9.3 9749 hsmexlem5 10365 wuncval2 10682 dprdspan 19804 tgcmp 22750 txcmplem1 22990 txcmplem2 22991 xkococnlem 23008 alexsubALT 23400 bcth3 24693 ovolfioo 24829 ovolficc 24830 voliunlem2 24913 voliunlem3 24914 volsup 24918 uniiccdif 24940 uniioovol 24941 uniiccvol 24942 uniioombllem2 24945 uniioombllem4 24948 volsup2 24967 itg1climres 25077 itg2monolem1 25113 itg2gt0 25123 sigapildsys 32701 omssubadd 32840 carsgclctunlem3 32860 pibt2 35878 volsupnfl 36113 hbt 41434 ovolval4lem1 44861 ovolval5lem3 44866 ovnovollem1 44868 ovnovollem2 44869 |
Copyright terms: Public domain | W3C validator |