Theorem elfvex 6862

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3438  dom cdm 5623  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-dm 5633  df-iota 6442  df-fv 6494

This theorem is referenced by:  elfvexd  6863  fviss  6904  fiin  9331  elharval  9472  elfzp12  13524  ismre  17510  ismri  17555  isacs  17575  oppccofval  17640  mulgnngsum  18976  gexid  19478  efgrcl  19612  islss  20855  thlle  21622  islbs4  21757  istopon  22815  fgval  23773  fgcl  23781  ufilen  23833  ustssxp  24108  ustbasel  24110  ustincl  24111  ustdiag  24112  ustinvel  24113  ustexhalf  24114  ustfilxp  24116  ustbas2  24129  trust  24133  utopval  24136  elutop  24137  restutop  24141  ustuqtop5  24149  isucn  24181  psmetdmdm  24209  psmetf  24210  psmet0  24212  psmettri2  24213  psmetres2  24218  ismet2  24237  xmetpsmet  24252  metustfbas  24461  metust  24462  iscmet  25200  ulmscl  26304  1vgrex  28965  wlkcompim  29595  clwlkcompim  29743  wwlkbp  29804  2wlkdlem7  29895  clwwlkbp  29947  3wlkdlem7  30128  metidval  33856  pstmval  33861  pstmxmet  33863  issiga  34078  insiga  34103  mvrsval  35477  mrsubcv  35482  mrsubccat  35490  mppsval  35544  topdifinffinlem  37320  istotbnd  37748  isbnd  37759  ismrc  42674  isnacs  42677  mzpcl1  42702  mzpcl2  42703  mzpf  42709  mzpadd  42711  mzpmul  42712  mzpsubmpt  42716  mzpnegmpt  42717  mzpexpmpt  42718  mzpindd  42719  mzpsubst  42721  mzpcompact2  42725  mzpcong  42945  sprel  47469  grtriprop  47924  clintop  48180  assintop  48181  clintopcllaw  48183  assintopcllaw  48184  assintopass  48186  oppcinito  49208  oppctermo  49209  oppczeroo  49210