Theorem elfvex 6908

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450  dom cdm 5647  ‘cfv 6527

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-dm 5657  df-iota 6483  df-fv 6535

This theorem is used by:  elfvexd  6909  fviss  6950  fiin  9392  elharval  9533  elfzp12  13706  ismre  17722  ismri  17767  isacs  17787  oppccofval  17852  mulgnngsum  19251  gexid  19757  efgrcl  19891  islss  21171  thlle  21965  islbs4  22100  istopon  23192  fgval  24151  fgcl  24159  ufilen  24211  ustssxp  24486  ustbasel  24488  ustincl  24489  ustdiag  24490  ustinvel  24491  ustexhalf  24492  ustfilxp  24494  ustbas2  24506  trust  24510  utopval  24513  elutop  24514  restutop  24518  ustuqtop5  24526  isucn  24558  psmetdmdm  24586  psmetf  24587  psmet0  24589  psmettri2  24590  psmetres2  24595  ismet2  24614  xmetpsmet  24629  metustfbas  24838  metust  24839  iscmet  25567  ulmscl  26670  1vgrex  29514  wlkcompim  30146  clwlkcompim  30301  wwlkbp  30364  2wlkdlem7  30455  clwwlkbp  30510  3wlkdlem7  30701  metidval  34456  pstmval  34461  pstmxmet  34463  issiga  34678  insiga  34704  mvrsval  36191  mrsubcv  36196  mrsubccat  36204  mppsval  36258  topdifinffinlem  38190  istotbnd  38623  isbnd  38634  ismrc  43650  isnacs  43653  mzpcl1  43678  mzpcl2  43679  mzpf  43685  mzpadd  43687  mzpmul  43688  mzpsubmpt  43692  mzpnegmpt  43693  mzpexpmpt  43694  mzpindd  43695  mzpsubst  43697  mzpcompact2  43701  mzpcong  43917  sprel  48488  grtriprop  48961  clintop  49227  assintop  49228  clintopcllaw  49230  assintopcllaw  49231  assintopass  49233  oppcinito  50265  oppctermo  50266  oppczeroo  50267