Theorem elfvex 6866

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 6865	. 2 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹)
2	1	elexd 3462	1 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3438  dom cdm 5621  ‘cfv 6489

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-dm 5631  df-iota 6445  df-fv 6497

This theorem is referenced by:  elfvexd  6867  fviss  6908  fiin  9316  elharval  9457  elfzp12  13513  ismre  17502  ismri  17547  isacs  17567  oppccofval  17632  mulgnngsum  19002  gexid  19503  efgrcl  19637  islss  20877  thlle  21644  islbs4  21779  istopon  22837  fgval  23795  fgcl  23803  ufilen  23855  ustssxp  24130  ustbasel  24132  ustincl  24133  ustdiag  24134  ustinvel  24135  ustexhalf  24136  ustfilxp  24138  ustbas2  24150  trust  24154  utopval  24157  elutop  24158  restutop  24162  ustuqtop5  24170  isucn  24202  psmetdmdm  24230  psmetf  24231  psmet0  24233  psmettri2  24234  psmetres2  24239  ismet2  24258  xmetpsmet  24273  metustfbas  24482  metust  24483  iscmet  25221  ulmscl  26325  1vgrex  28991  wlkcompim  29621  clwlkcompim  29769  wwlkbp  29830  2wlkdlem7  29921  clwwlkbp  29976  3wlkdlem7  30157  metidval  33914  pstmval  33919  pstmxmet  33921  issiga  34136  insiga  34161  mvrsval  35560  mrsubcv  35565  mrsubccat  35573  mppsval  35627  topdifinffinlem  37402  istotbnd  37819  isbnd  37830  ismrc  42808  isnacs  42811  mzpcl1  42836  mzpcl2  42837  mzpf  42843  mzpadd  42845  mzpmul  42846  mzpsubmpt  42850  mzpnegmpt  42851  mzpexpmpt  42852  mzpindd  42853  mzpsubst  42855  mzpcompact2  42859  mzpcong  43079  sprel  47598  grtriprop  48055  clintop  48322  assintop  48323  clintopcllaw  48325  assintopcllaw  48326  assintopass  48328  oppcinito  49350  oppctermo  49351  oppczeroo  49352