Theorem elfvex 6870

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3441  dom cdm 5625  ‘cfv 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-dm 5635  df-iota 6449  df-fv 6501

This theorem is referenced by:  elfvexd  6871  fviss  6912  fiin  9329  elharval  9470  elfzp12  13523  ismre  17513  ismri  17558  isacs  17578  oppccofval  17643  mulgnngsum  19013  gexid  19514  efgrcl  19648  islss  20889  thlle  21656  islbs4  21791  istopon  22860  fgval  23818  fgcl  23826  ufilen  23878  ustssxp  24153  ustbasel  24155  ustincl  24156  ustdiag  24157  ustinvel  24158  ustexhalf  24159  ustfilxp  24161  ustbas2  24173  trust  24177  utopval  24180  elutop  24181  restutop  24185  ustuqtop5  24193  isucn  24225  psmetdmdm  24253  psmetf  24254  psmet0  24256  psmettri2  24257  psmetres2  24262  ismet2  24281  xmetpsmet  24296  metustfbas  24505  metust  24506  iscmet  25244  ulmscl  26348  1vgrex  29058  wlkcompim  29688  clwlkcompim  29836  wwlkbp  29897  2wlkdlem7  29988  clwwlkbp  30043  3wlkdlem7  30224  metidval  34028  pstmval  34033  pstmxmet  34035  issiga  34250  insiga  34275  mvrsval  35680  mrsubcv  35685  mrsubccat  35693  mppsval  35747  topdifinffinlem  37523  istotbnd  37941  isbnd  37952  ismrc  42979  isnacs  42982  mzpcl1  43007  mzpcl2  43008  mzpf  43014  mzpadd  43016  mzpmul  43017  mzpsubmpt  43021  mzpnegmpt  43022  mzpexpmpt  43023  mzpindd  43024  mzpsubst  43026  mzpcompact2  43030  mzpcong  43250  sprel  47766  grtriprop  48223  clintop  48490  assintop  48491  clintopcllaw  48493  assintopcllaw  48494  assintopass  48496  oppcinito  49516  oppctermo  49517  oppczeroo  49518