| 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 4340 | . 2 ⊢ (𝐴 ∈ (𝐹‘𝐵) → ¬ (𝐹‘𝐵) = ∅) | |
| 2 | ndmfv 6941 | . 2 ⊢ (¬ 𝐵 ∈ dom 𝐹 → (𝐹‘𝐵) = ∅) | |
| 3 | 1, 2 | nsyl2 141 | 1 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 ∅c0 4333 dom cdm 5685 ‘cfv 6561 |
| 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 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-dm 5695 df-iota 6514 df-fv 6569 |
| This theorem is referenced by: elfvex 6944 elfvmptrab1w 7043 fveqdmss 7098 eldmrexrnb 7112 elunirn2OLD 7273 elmpocl 7674 elovmpt3rab1 7693 mpoxeldm 8236 mpoxopn0yelv 8238 mpoxopxnop0 8240 r1pwss 9824 rankwflemb 9833 r1elwf 9836 rankr1ai 9838 rankdmr1 9841 rankr1ag 9842 rankr1c 9861 r1pwcl 9887 cardne 10005 cardsdomelir 10013 r1wunlim 10777 eluzel2 12883 acsfiel 17697 homarcl2 18080 arwrcl 18089 pleval2i 18381 acsdrscl 18591 acsficl 18592 submgmrcl 18708 gsumws1 18851 cntzrcl 19345 smndlsmidm 19674 eldprd 20024 isunit 20373 isirred 20419 lbsss 21076 lbssp 21078 lbsind 21079 elocv 21686 cssi 21702 linds1 21830 linds2 21831 lindsind 21837 ply1frcl 22322 eltg4i 22967 eltg3 22969 tg1 22971 tg2 22972 cldrcl 23034 neiss2 23109 lmrcl 23239 iscnp2 23247 kqtop 23753 fbasne0 23838 0nelfb 23839 fbsspw 23840 fbasssin 23844 fbun 23848 trfbas2 23851 trfbas 23852 isfil 23855 filss 23861 fbasweak 23873 fgval 23878 elfg 23879 fgcl 23886 isufil 23911 ufilss 23913 trufil 23918 fmval 23951 elfm3 23958 fmfnfmlem4 23965 fmfnfm 23966 metflem 24338 xmetf 24339 xmeteq0 24348 xmettri2 24350 xmetres2 24371 blfvalps 24393 blvalps 24395 blval 24396 blfps 24416 blf 24417 isxms2 24458 tmslem 24494 tmslemOLD 24495 lmmbr2 25293 lmmbrf 25296 fmcfil 25306 iscau2 25311 iscauf 25314 caucfil 25317 cmetcaulem 25322 iscmet3 25327 cfilresi 25329 caussi 25331 causs 25332 metcld2 25341 cmetss 25350 bcthlem1 25358 bcth3 25365 cpncn 25972 cpnres 25973 madebdayim 27926 oldbdayim 27927 tglngne 28558 wlkdlem3 29702 1wlkdlem3 30158 fpwrelmap 32744 brsiga 34184 measbase 34198 cvmsrcl 35269 snmlval 35336 fneuni 36348 uncf 37606 unccur 37610 caures 37767 ismtyval 37807 isismty 37808 heiborlem10 37827 eldiophb 42768 elmnc 43148 elbigofrcl 48471 |
| Copyright terms: Public domain | W3C validator |