Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fvelrn | Structured version Visualization version GIF version |
Description: A function's value belongs to its range. (Contributed by NM, 14-Oct-1996.) |
Ref | Expression |
---|---|
fvelrn | ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2899 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ dom 𝐹 ↔ 𝐴 ∈ dom 𝐹)) | |
2 | 1 | anbi2d 630 | . . . 4 ⊢ (𝑥 = 𝐴 → ((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) ↔ (Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹))) |
3 | fveq2 6667 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) | |
4 | 3 | eleq1d 2896 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) ∈ ran 𝐹 ↔ (𝐹‘𝐴) ∈ ran 𝐹)) |
5 | 2, 4 | imbi12d 347 | . . 3 ⊢ (𝑥 = 𝐴 → (((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ran 𝐹) ↔ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹))) |
6 | funfvop 6817 | . . . . 5 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) → 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹) | |
7 | vex 3496 | . . . . . 6 ⊢ 𝑥 ∈ V | |
8 | opeq1 4800 | . . . . . . 7 ⊢ (𝑦 = 𝑥 → 〈𝑦, (𝐹‘𝑥)〉 = 〈𝑥, (𝐹‘𝑥)〉) | |
9 | 8 | eleq1d 2896 | . . . . . 6 ⊢ (𝑦 = 𝑥 → (〈𝑦, (𝐹‘𝑥)〉 ∈ 𝐹 ↔ 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹)) |
10 | 7, 9 | spcev 3606 | . . . . 5 ⊢ (〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹 → ∃𝑦〈𝑦, (𝐹‘𝑥)〉 ∈ 𝐹) |
11 | 6, 10 | syl 17 | . . . 4 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) → ∃𝑦〈𝑦, (𝐹‘𝑥)〉 ∈ 𝐹) |
12 | fvex 6680 | . . . . 5 ⊢ (𝐹‘𝑥) ∈ V | |
13 | 12 | elrn2 5818 | . . . 4 ⊢ ((𝐹‘𝑥) ∈ ran 𝐹 ↔ ∃𝑦〈𝑦, (𝐹‘𝑥)〉 ∈ 𝐹) |
14 | 11, 13 | sylibr 236 | . . 3 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ran 𝐹) |
15 | 5, 14 | vtoclg 3566 | . 2 ⊢ (𝐴 ∈ dom 𝐹 → ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹)) |
16 | 15 | anabsi7 669 | 1 ⊢ ((Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1536 ∃wex 1779 ∈ wcel 2113 〈cop 4570 dom cdm 5552 ran crn 5553 Fun wfun 6346 ‘cfv 6352 |
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 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2792 ax-sep 5200 ax-nul 5207 ax-pr 5327 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1084 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2799 df-cleq 2813 df-clel 2892 df-nfc 2962 df-ral 3142 df-rex 3143 df-rab 3146 df-v 3495 df-sbc 3771 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4465 df-sn 4565 df-pr 4567 df-op 4571 df-uni 4836 df-br 5064 df-opab 5126 df-id 5457 df-xp 5558 df-rel 5559 df-cnv 5560 df-co 5561 df-dm 5562 df-rn 5563 df-iota 6311 df-fun 6354 df-fn 6355 df-fv 6360 |
This theorem is referenced by: nelrnfvne 6842 fnfvelrn 6845 eldmrexrn 6854 fvn0fvelrn 6922 funfvima 6989 elunirn 7007 rankwflemb 9219 dfac9 9559 fin1a2lem6 9824 gsumpropd2lem 17885 iedgedg 26833 usgredg3 26996 ushgredgedg 27009 ushgredgedgloop 27011 subgruhgredgd 27064 edginwlk 27414 iedginwlk 27416 opfv 30393 fnpreimac 30416 ccatf1 30625 swrdrn2 30628 funeldmb 33030 nofv 33188 sltres 33193 nolt02olem 33222 nosupno 33227 bj-elccinfty 34523 bj-minftyccb 34534 icoreunrn 34667 indexdom 35045 diaclN 38222 dia1elN 38226 docaclN 38296 dibclN 38334 dfac21 39741 harval3 39978 gneispace 40558 cncmpmax 41363 icccncfext 42244 stoweidlem27 42386 stoweidlem29 42388 stoweidlem59 42418 fourierdlem20 42486 fourierdlem63 42528 fourierdlem76 42541 fourierdlem82 42547 fourierdlem93 42558 fourierdlem113 42578 fge0iccico 42726 sge0sn 42735 sge0tsms 42736 sge0cl 42737 sge0isum 42783 hoicvr 42904 funressndmfvrn 43353 afvelrn 43441 isomushgr 44065 ushrisomgr 44080 suppdm 44639 |
Copyright terms: Public domain | W3C validator |