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 4234 | . 2 ⊢ (𝐴 ∈ (𝐹‘𝐵) → ¬ (𝐹‘𝐵) = ∅) | |
2 | ndmfv 6725 | . 2 ⊢ (¬ 𝐵 ∈ dom 𝐹 → (𝐹‘𝐵) = ∅) | |
3 | 1, 2 | nsyl2 143 | 1 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ∈ wcel 2112 ∅c0 4223 dom cdm 5536 ‘cfv 6358 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-sep 5177 ax-nul 5184 ax-pr 5307 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-ne 2933 df-ral 3056 df-rex 3057 df-rab 3060 df-v 3400 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4224 df-if 4426 df-sn 4528 df-pr 4530 df-op 4534 df-uni 4806 df-br 5040 df-dm 5546 df-iota 6316 df-fv 6366 |
This theorem is referenced by: elfvex 6728 elfvmptrab1w 6822 fveqdmss 6877 eldmrexrnb 6889 elmpocl 7425 elovmpt3rab1 7443 mpoxeldm 7931 mpoxopn0yelv 7933 mpoxopxnop0 7935 r1pwss 9365 rankwflemb 9374 r1elwf 9377 rankr1ai 9379 rankdmr1 9382 rankr1ag 9383 rankr1c 9402 r1pwcl 9428 cardne 9546 cardsdomelir 9554 r1wunlim 10316 eluzel2 12408 acsfiel 17111 homarcl2 17495 arwrcl 17504 pleval2i 17796 acsdrscl 18006 acsficl 18007 gsumws1 18218 cntzrcl 18675 smndlsmidm 18999 eldprd 19345 isunit 19629 isirred 19671 lbsss 20068 lbssp 20070 lbsind 20071 elocv 20584 cssi 20600 linds1 20726 linds2 20727 lindsind 20733 ply1frcl 21188 eltg4i 21811 eltg3 21813 tg1 21815 tg2 21816 cldrcl 21877 neiss2 21952 lmrcl 22082 iscnp2 22090 kqtop 22596 fbasne0 22681 0nelfb 22682 fbsspw 22683 fbasssin 22687 fbun 22691 trfbas2 22694 trfbas 22695 isfil 22698 filss 22704 fbasweak 22716 fgval 22721 elfg 22722 fgcl 22729 isufil 22754 ufilss 22756 trufil 22761 fmval 22794 elfm3 22801 fmfnfmlem4 22808 fmfnfm 22809 elrnust 23076 metflem 23180 xmetf 23181 xmeteq0 23190 xmettri2 23192 xmetres2 23213 blfvalps 23235 blvalps 23237 blval 23238 blfps 23258 blf 23259 isxms2 23300 tmslem 23334 metuval 23401 lmmbr2 24110 lmmbrf 24113 fmcfil 24123 iscau2 24128 iscauf 24131 caucfil 24134 cmetcaulem 24139 iscmet3 24144 cfilresi 24146 caussi 24148 causs 24149 metcld2 24158 cmetss 24167 bcthlem1 24175 bcth3 24182 cpncn 24787 cpnres 24788 tglngne 26595 wlkdlem3 27726 1wlkdlem3 28176 elunirn2 30662 fpwrelmap 30742 metidval 31508 pstmval 31513 brsiga 31817 measbase 31831 cvmsrcl 32893 snmlval 32960 madebdayim 33756 oldbdayim 33757 fneuni 34222 uncf 35442 unccur 35446 caures 35604 ismtyval 35644 isismty 35645 heiborlem10 35664 eldiophb 40223 elmnc 40605 submgmrcl 44952 elbigofrcl 45512 |
Copyright terms: Public domain | W3C validator |