Theorem elfvex 6876

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430  dom cdm 5631  ‘cfv 6499

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 5242  ax-pr 5376

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 5641  df-iota 6455  df-fv 6507

This theorem is referenced by:  elfvexd  6877  fviss  6918  fiin  9335  elharval  9476  elfzp12  13557  ismre  17552  ismri  17597  isacs  17617  oppccofval  17682  mulgnngsum  19055  gexid  19556  efgrcl  19690  islss  20929  thlle  21677  islbs4  21812  istopon  22877  fgval  23835  fgcl  23843  ufilen  23895  ustssxp  24170  ustbasel  24172  ustincl  24173  ustdiag  24174  ustinvel  24175  ustexhalf  24176  ustfilxp  24178  ustbas2  24190  trust  24194  utopval  24197  elutop  24198  restutop  24202  ustuqtop5  24210  isucn  24242  psmetdmdm  24270  psmetf  24271  psmet0  24273  psmettri2  24274  psmetres2  24279  ismet2  24298  xmetpsmet  24313  metustfbas  24522  metust  24523  iscmet  25251  ulmscl  26344  1vgrex  29071  wlkcompim  29700  clwlkcompim  29848  wwlkbp  29909  2wlkdlem7  30000  clwwlkbp  30055  3wlkdlem7  30236  metidval  34034  pstmval  34039  pstmxmet  34041  issiga  34256  insiga  34281  mvrsval  35687  mrsubcv  35692  mrsubccat  35700  mppsval  35754  topdifinffinlem  37663  istotbnd  38090  isbnd  38101  ismrc  43133  isnacs  43136  mzpcl1  43161  mzpcl2  43162  mzpf  43168  mzpadd  43170  mzpmul  43171  mzpsubmpt  43175  mzpnegmpt  43176  mzpexpmpt  43177  mzpindd  43178  mzpsubst  43180  mzpcompact2  43184  mzpcong  43400  sprel  47938  grtriprop  48411  clintop  48678  assintop  48679  clintopcllaw  48681  assintopcllaw  48682  assintopass  48684  oppcinito  49704  oppctermo  49705  oppczeroo  49706