![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elfvdm | Structured version Visualization version Unicode version |
Description: If a function value has a member, the argument belongs to the domain. (Contributed by NM, 12-Feb-2007.) |
Ref | Expression |
---|---|
elfvdm |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ne0i 3728 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ndmfv 5903 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | necon1ai 2670 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | syl 17 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-nul 4527 ax-pow 4579 |
This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-rab 2765 df-v 3033 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4191 df-br 4396 df-dm 4849 df-iota 5553 df-fv 5597 |
This theorem is referenced by: elfvex 5906 fveqdmss 6032 eldmrexrnb 6044 elmpt2cl 6530 elovmpt3rab1 6546 mpt2xeldm 6976 mpt2xopn0yelv 6978 mpt2xopxnop0 6980 r1pwss 8273 rankwflemb 8282 r1elwf 8285 rankr1ai 8287 rankdmr1 8290 rankr1ag 8291 rankr1c 8310 r1pwcl 8336 cardne 8417 cardsdomelir 8425 r1wunlim 9180 eluzel2 11187 bitsval 14476 acsfiel 15638 subcrcl 15799 homarcl2 16008 arwrcl 16017 pleval2i 16288 acsdrscl 16494 acsficl 16495 submrcl 16671 gsumws1 16701 issubg 16895 isnsg 16924 cntzrcl 17059 eldprd 17714 isunit 17963 isirred 18005 abvrcl 18127 lbsss 18378 lbssp 18380 lbsind 18381 ply1frcl 18984 elocv 19308 cssi 19324 isobs 19360 linds1 19445 linds2 19446 lindsind 19452 eltg4i 20052 eltg3 20054 tg1 20056 tg2 20057 cldrcl 20118 neiss2 20194 lmrcl 20324 iscnp2 20332 islocfin 20609 kgeni 20629 kqtop 20837 fbasne0 20923 0nelfb 20924 fbsspw 20925 fbasssin 20929 fbun 20933 trfbas2 20936 trfbas 20937 isfil 20940 filss 20946 fbasweak 20958 fgval 20963 elfg 20964 fgcl 20971 isufil 20996 ufilss 20998 trufil 21003 fmval 21036 elfm3 21043 fmfnfmlem4 21050 fmfnfm 21051 elrnust 21317 metflem 21421 xmetf 21422 xmeteq0 21431 xmettri2 21433 xmetres2 21454 blfvalps 21476 blvalps 21478 blval 21479 blfps 21499 blf 21500 isxms2 21541 tmslem 21575 metuval 21642 isphtpc 22103 lmmbr2 22307 lmmbrf 22310 cfili 22316 fmcfil 22320 cfilfcls 22322 iscau2 22325 iscauf 22328 caucfil 22331 cmetcaulem 22336 iscmet3 22341 cfilresi 22343 caussi 22345 causs 22346 metcld2 22354 cmetss 22362 bcthlem1 22370 bcth3 22377 cpncn 22969 cpnres 22970 plybss 23227 tglngne 24674 2trllemF 25358 constr1trl 25397 issubgo 26112 elunirn2 28326 fpwrelmap 28393 metidval 28767 pstmval 28772 brsiga 29079 measbase 29093 cvmsrcl 30059 snmlval 30126 fneuni 31074 caures 32153 ismtyval 32196 isismty 32197 heiborlem10 32216 eldiophb 35670 elmnc 36066 issdrg 36134 1wlkdlem3 39884 11wlkdlem3 40027 submgmrcl 40290 elbigofrcl 40869 |
Copyright terms: Public domain | W3C validator |