Theorem elfvex 6869

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

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3432  dom cdm 5625  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-dm 5635  df-iota 6448  df-fv 6500

This theorem is referenced by:  elfvexd  6870  fviss  6911  fiin  9332  elharval  9473  elfzp12  13555  ismre  17550  ismri  17595  isacs  17615  oppccofval  17680  mulgnngsum  19053  gexid  19554  efgrcl  19688  islss  20931  thlle  21679  islbs4  21814  istopon  22902  fgval  23860  fgcl  23868  ufilen  23920  ustssxp  24195  ustbasel  24197  ustincl  24198  ustdiag  24199  ustinvel  24200  ustexhalf  24201  ustfilxp  24203  ustbas2  24215  trust  24219  utopval  24222  elutop  24223  restutop  24227  ustuqtop5  24235  isucn  24267  psmetdmdm  24295  psmetf  24296  psmet0  24298  psmettri2  24299  psmetres2  24304  ismet2  24323  xmetpsmet  24338  metustfbas  24547  metust  24548  iscmet  25276  ulmscl  26369  1vgrex  29096  wlkcompim  29725  clwlkcompim  29873  wwlkbp  29934  2wlkdlem7  30025  clwwlkbp  30080  3wlkdlem7  30261  metidval  34081  pstmval  34086  pstmxmet  34088  issiga  34303  insiga  34328  mvrsval  35734  mrsubcv  35739  mrsubccat  35747  mppsval  35801  topdifinffinlem  37710  istotbnd  38137  isbnd  38148  ismrc  43151  isnacs  43154  mzpcl1  43179  mzpcl2  43180  mzpf  43186  mzpadd  43188  mzpmul  43189  mzpsubmpt  43193  mzpnegmpt  43194  mzpexpmpt  43195  mzpindd  43196  mzpsubst  43198  mzpcompact2  43202  mzpcong  43418  sprel  47960  grtriprop  48433  clintop  48700  assintop  48701  clintopcllaw  48703  assintopcllaw  48704  assintopass  48706  oppcinito  49726  oppctermo  49727  oppczeroo  49728