Theorem elfvex 6867

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430  dom cdm 5622  ‘cfv 6490

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 5241  ax-pr 5368

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-dm 5632  df-iota 6446  df-fv 6498

This theorem is referenced by:  elfvexd  6868  fviss  6909  fiin  9326  elharval  9467  elfzp12  13546  ismre  17541  ismri  17586  isacs  17606  oppccofval  17671  mulgnngsum  19044  gexid  19545  efgrcl  19679  islss  20918  thlle  21685  islbs4  21820  istopon  22886  fgval  23844  fgcl  23852  ufilen  23904  ustssxp  24179  ustbasel  24181  ustincl  24182  ustdiag  24183  ustinvel  24184  ustexhalf  24185  ustfilxp  24187  ustbas2  24199  trust  24203  utopval  24206  elutop  24207  restutop  24211  ustuqtop5  24219  isucn  24251  psmetdmdm  24279  psmetf  24280  psmet0  24282  psmettri2  24283  psmetres2  24288  ismet2  24307  xmetpsmet  24322  metustfbas  24531  metust  24532  iscmet  25260  ulmscl  26359  1vgrex  29090  wlkcompim  29720  clwlkcompim  29868  wwlkbp  29929  2wlkdlem7  30020  clwwlkbp  30075  3wlkdlem7  30256  metidval  34055  pstmval  34060  pstmxmet  34062  issiga  34277  insiga  34302  mvrsval  35708  mrsubcv  35713  mrsubccat  35721  mppsval  35775  topdifinffinlem  37674  istotbnd  38101  isbnd  38112  ismrc  43144  isnacs  43147  mzpcl1  43172  mzpcl2  43173  mzpf  43179  mzpadd  43181  mzpmul  43182  mzpsubmpt  43186  mzpnegmpt  43187  mzpexpmpt  43188  mzpindd  43189  mzpsubst  43191  mzpcompact2  43195  mzpcong  43415  sprel  47941  grtriprop  48414  clintop  48681  assintop  48682  clintopcllaw  48684  assintopcllaw  48685  assintopass  48687  oppcinito  49707  oppctermo  49708  oppczeroo  49709