![]() |
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, then the argument is a set. (An artifact of our function value definition.) (Contributed by Mario Carneiro, 6-Nov-2015.) |
Ref | Expression |
---|---|
elfvex | ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfvdm 6570 | . 2 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹) | |
2 | 1 | elexd 3457 | 1 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2081 Vcvv 3437 dom cdm 5443 ‘cfv 6225 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 ax-nul 5101 ax-pow 5157 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-dm 5453 df-iota 6189 df-fv 6233 |
This theorem is referenced by: elfvexd 6572 fviss 6608 fiin 8732 elharval 8873 elfzp12 12836 ismre 16690 ismri 16731 isacs 16751 oppccofval 16815 gexid 18436 efgrcl 18568 islss 19396 thlle 20523 islbs4 20658 istopon 21204 fgval 22162 fgcl 22170 ufilen 22222 ustssxp 22496 ustbasel 22498 ustincl 22499 ustdiag 22500 ustinvel 22501 ustexhalf 22502 ustfilxp 22504 ustbas2 22517 trust 22521 utopval 22524 elutop 22525 restutop 22529 ustuqtop5 22537 isucn 22570 psmetdmdm 22598 psmetf 22599 psmet0 22601 psmettri2 22602 psmetres2 22607 ismet2 22626 xmetpsmet 22641 metustfbas 22850 metust 22851 iscmet 23570 ulmscl 24650 1vgrex 26470 wlkcompim 27096 clwlkcompim 27248 wwlkbp 27306 2wlkdlem7 27398 clwwlkbp 27450 3wlkdlem7 27632 metidval 30747 pstmval 30752 pstmxmet 30754 issiga 30988 insiga 31013 mvrsval 32361 mrsubcv 32366 mrsubccat 32374 mppsval 32428 topdifinffinlem 34178 istotbnd 34598 isbnd 34609 ismrc 38802 isnacs 38805 mzpcl1 38830 mzpcl2 38831 mzpf 38837 mzpadd 38839 mzpmul 38840 mzpsubmpt 38844 mzpnegmpt 38845 mzpexpmpt 38846 mzpindd 38847 mzpsubst 38849 mzpcompact2 38853 mzpcong 39073 sprel 43148 clintop 43613 assintop 43614 clintopcllaw 43616 assintopcllaw 43617 assintopass 43619 |
Copyright terms: Public domain | W3C validator |