![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elfvex | Structured version Visualization version GIF version |
Description: If a function value has a member, the argument is a set. (Contributed by Mario Carneiro, 6-Nov-2015.) |
Ref | Expression |
---|---|
elfvex | ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfvdm 6362 | . 2 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹) | |
2 | elex 3364 | . 2 ⊢ (𝐵 ∈ dom 𝐹 → 𝐵 ∈ V) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2145 Vcvv 3351 dom cdm 5250 ‘cfv 6032 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-nul 4924 ax-pow 4975 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-dif 3727 df-un 3729 df-in 3731 df-ss 3738 df-nul 4065 df-if 4227 df-sn 4318 df-pr 4320 df-op 4324 df-uni 4576 df-br 4788 df-dm 5260 df-iota 5995 df-fv 6040 |
This theorem is referenced by: elfvexd 6364 fviss 6399 fiin 8485 elharval 8625 elfzp12 12627 ismre 16459 ismri 16500 isacs 16520 oppccofval 16584 gexid 18204 efgrcl 18336 islss 19146 thlle 20259 islbs4 20389 istopon 20938 fgval 21895 fgcl 21903 ufilen 21955 ustssxp 22229 ustbasel 22231 ustincl 22232 ustdiag 22233 ustinvel 22234 ustexhalf 22235 ustfilxp 22237 ustbas2 22250 trust 22254 utopval 22257 elutop 22258 restutop 22262 ustuqtop5 22270 isucn 22303 psmetdmdm 22331 psmetf 22332 psmet0 22334 psmettri2 22335 psmetres2 22340 ismet2 22359 xmetpsmet 22374 metustfbas 22583 metust 22584 iscmet 23302 ulmscl 24354 1vgrex 26104 wlkcompim 26763 clwlkcompim 26912 wwlkbp 26970 2wlkdlem7 27080 clwwlkbp 27136 3wlkdlem7 27347 metidval 30274 pstmval 30279 pstmxmet 30281 issiga 30515 insiga 30541 mvrsval 31741 mrsubcv 31746 mrsubccat 31754 mppsval 31808 topdifinffinlem 33533 istotbnd 33901 isbnd 33912 ismrc 37791 isnacs 37794 mzpcl1 37819 mzpcl2 37820 mzpf 37826 mzpadd 37828 mzpmul 37829 mzpsubmpt 37833 mzpnegmpt 37834 mzpexpmpt 37835 mzpindd 37836 mzpsubst 37838 mzpcompact2 37842 mzpcong 38066 sprel 42263 clintop 42373 assintop 42374 clintopcllaw 42376 assintopcllaw 42377 assintopass 42379 |
Copyright terms: Public domain | W3C validator |