| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > elfvdm | Structured version Visualization version GIF version | ||
| Description: If a function value has a member, then the argument belongs to the domain. (An artifact of our function value definition.) (Contributed by NM, 12-Feb-2007.) (Proof shortened by BJ, 22-Oct-2022.) |
| Ref | Expression |
|---|---|
| elfvdm | ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | n0i 4281 | . 2 ⊢ (𝐴 ∈ (𝐹‘𝐵) → ¬ (𝐹‘𝐵) = ∅) | |
| 2 | ndmfv 6868 | . 2 ⊢ (¬ 𝐵 ∈ dom 𝐹 → (𝐹‘𝐵) = ∅) | |
| 3 | 1, 2 | nsyl2 141 | 1 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 ∅c0 4274 dom cdm 5626 ‘cfv 6494 |
| 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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2709 ax-nul 5242 ax-pr 5372 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-ne 2934 df-rab 3391 df-v 3432 df-dif 3893 df-un 3895 df-ss 3907 df-nul 4275 df-if 4468 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-br 5087 df-dm 5636 df-iota 6450 df-fv 6502 |
| This theorem is referenced by: elfvex 6871 elfvmptrab1w 6971 fveqdmss 7026 eldmrexrnb 7040 elmpocl 7603 elovmpt3rab1 7622 mpoxeldm 8156 mpoxopn0yelv 8158 mpoxopxnop0 8160 r1pwss 9703 rankwflemb 9712 r1elwf 9715 rankr1ai 9717 rankdmr1 9720 rankr1ag 9721 rankr1c 9740 r1pwcl 9766 cardne 9884 cardsdomelir 9892 r1wunlim 10655 eluzel2 12788 acsfiel 17615 homarcl2 17997 arwrcl 18006 pleval2i 18295 acsdrscl 18507 acsficl 18508 submgmrcl 18658 gsumws1 18801 cntzrcl 19297 smndlsmidm 19626 eldprd 19976 isunit 20348 isirred 20394 lbsss 21068 lbssp 21070 lbsind 21071 elocv 21662 cssi 21678 linds1 21804 linds2 21805 lindsind 21811 ply1frcl 22297 eltg4i 22939 eltg3 22941 tg1 22943 tg2 22944 cldrcl 23005 neiss2 23080 lmrcl 23210 iscnp2 23218 kqtop 23724 fbasne0 23809 0nelfb 23810 fbsspw 23811 fbasssin 23815 fbun 23819 trfbas2 23822 trfbas 23823 isfil 23826 filss 23832 fbasweak 23844 fgval 23849 elfg 23850 fgcl 23857 isufil 23882 ufilss 23884 trufil 23889 fmval 23922 elfm3 23929 fmfnfmlem4 23936 fmfnfm 23937 metflem 24307 xmetf 24308 xmeteq0 24317 xmettri2 24319 xmetres2 24340 blfvalps 24362 blvalps 24364 blval 24365 blfps 24385 blf 24386 isxms2 24427 tmslem 24461 lmmbr2 25240 lmmbrf 25243 fmcfil 25253 iscau2 25258 iscauf 25261 caucfil 25264 cmetcaulem 25269 iscmet3 25274 cfilresi 25276 caussi 25278 causs 25279 metcld2 25288 cmetss 25297 bcthlem1 25305 bcth3 25312 cpncn 25917 cpnres 25918 madebdayim 27898 oldbdayim 27899 newbdayim 27913 cutminmax 27946 tglngne 28636 wlkdlem3 29770 1wlkdlem3 30228 fpwrelmap 32825 brsiga 34347 measbase 34361 r1elcl 35261 cvmsrcl 35466 snmlval 35533 fneuni 36549 uncf 37938 unccur 37942 caures 38099 ismtyval 38139 isismty 38140 heiborlem10 38159 eldiophb 43207 elmnc 43586 elbigofrcl 49042 cicrcl2 49534 cic1st2nd 49538 eloppf 49624 |
| Copyright terms: Public domain | W3C validator |