Theorem elfvex 6789

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3422  dom cdm 5580  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-dm 5590  df-iota 6376  df-fv 6426

This theorem is referenced by:  elfvexd  6790  fviss  6827  fiin  9111  elharval  9250  elfzp12  13264  ismre  17216  ismri  17257  isacs  17277  oppccofval  17343  mulgnngsum  18624  gexid  19101  efgrcl  19236  islss  20111  thlle  20814  islbs4  20949  istopon  21969  fgval  22929  fgcl  22937  ufilen  22989  ustssxp  23264  ustbasel  23266  ustincl  23267  ustdiag  23268  ustinvel  23269  ustexhalf  23270  ustfilxp  23272  ustbas2  23285  trust  23289  utopval  23292  elutop  23293  restutop  23297  ustuqtop5  23305  isucn  23338  psmetdmdm  23366  psmetf  23367  psmet0  23369  psmettri2  23370  psmetres2  23375  ismet2  23394  xmetpsmet  23409  metustfbas  23619  metust  23620  iscmet  24353  ulmscl  25443  1vgrex  27275  wlkcompim  27901  clwlkcompim  28049  wwlkbp  28107  2wlkdlem7  28198  clwwlkbp  28250  3wlkdlem7  28431  metidval  31742  pstmval  31747  pstmxmet  31749  issiga  31980  insiga  32005  mvrsval  33367  mrsubcv  33372  mrsubccat  33380  mppsval  33434  topdifinffinlem  35445  istotbnd  35854  isbnd  35865  ismrc  40439  isnacs  40442  mzpcl1  40467  mzpcl2  40468  mzpf  40474  mzpadd  40476  mzpmul  40477  mzpsubmpt  40481  mzpnegmpt  40482  mzpexpmpt  40483  mzpindd  40484  mzpsubst  40486  mzpcompact2  40490  mzpcong  40710  sprel  44824  clintop  45290  assintop  45291  clintopcllaw  45293  assintopcllaw  45294  assintopass  45296