Theorem elfvex 6703

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.)

Assertion

Ref	Expression
elfvex	⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ V)

Proof of Theorem elfvex

Step	Hyp	Ref	Expression
1		elfvdm 6702	. 2 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹)
2	1	elexd 3514	1 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3494  dom cdm 5555  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-nul 5210  ax-pow 5266

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-dm 5565  df-iota 6314  df-fv 6363

This theorem is referenced by:  elfvexd  6704  fviss  6741  fiin  8886  elharval  9027  elfzp12  12987  ismre  16861  ismri  16902  isacs  16922  oppccofval  16986  mulgnngsum  18233  gexid  18706  efgrcl  18841  islss  19706  thlle  20841  islbs4  20976  istopon  21520  fgval  22478  fgcl  22486  ufilen  22538  ustssxp  22813  ustbasel  22815  ustincl  22816  ustdiag  22817  ustinvel  22818  ustexhalf  22819  ustfilxp  22821  ustbas2  22834  trust  22838  utopval  22841  elutop  22842  restutop  22846  ustuqtop5  22854  isucn  22887  psmetdmdm  22915  psmetf  22916  psmet0  22918  psmettri2  22919  psmetres2  22924  ismet2  22943  xmetpsmet  22958  metustfbas  23167  metust  23168  iscmet  23887  ulmscl  24967  1vgrex  26787  wlkcompim  27413  clwlkcompim  27561  wwlkbp  27619  2wlkdlem7  27711  clwwlkbp  27763  3wlkdlem7  27945  metidval  31130  pstmval  31135  pstmxmet  31137  issiga  31371  insiga  31396  mvrsval  32752  mrsubcv  32757  mrsubccat  32765  mppsval  32819  topdifinffinlem  34631  istotbnd  35062  isbnd  35073  ismrc  39318  isnacs  39321  mzpcl1  39346  mzpcl2  39347  mzpf  39353  mzpadd  39355  mzpmul  39356  mzpsubmpt  39360  mzpnegmpt  39361  mzpexpmpt  39362  mzpindd  39363  mzpsubst  39365  mzpcompact2  39369  mzpcong  39589  sprel  43666  clintop  44135  assintop  44136  clintopcllaw  44138  assintopcllaw  44139  assintopass  44141