Theorem elfvex 6944

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480  dom cdm 5685  ‘cfv 6561

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-dm 5695  df-iota 6514  df-fv 6569

This theorem is referenced by:  elfvexd  6945  fviss  6986  fiin  9462  elharval  9601  elfzp12  13643  ismre  17633  ismri  17674  isacs  17694  oppccofval  17759  mulgnngsum  19097  gexid  19599  efgrcl  19733  islss  20932  thlle  21716  thlleOLD  21717  islbs4  21852  istopon  22918  fgval  23878  fgcl  23886  ufilen  23938  ustssxp  24213  ustbasel  24215  ustincl  24216  ustdiag  24217  ustinvel  24218  ustexhalf  24219  ustfilxp  24221  ustbas2  24234  trust  24238  utopval  24241  elutop  24242  restutop  24246  ustuqtop5  24254  isucn  24287  psmetdmdm  24315  psmetf  24316  psmet0  24318  psmettri2  24319  psmetres2  24324  ismet2  24343  xmetpsmet  24358  metustfbas  24570  metust  24571  iscmet  25318  ulmscl  26422  1vgrex  29019  wlkcompim  29650  clwlkcompim  29800  wwlkbp  29861  2wlkdlem7  29952  clwwlkbp  30004  3wlkdlem7  30185  metidval  33889  pstmval  33894  pstmxmet  33896  issiga  34113  insiga  34138  mvrsval  35510  mrsubcv  35515  mrsubccat  35523  mppsval  35577  topdifinffinlem  37348  istotbnd  37776  isbnd  37787  ismrc  42712  isnacs  42715  mzpcl1  42740  mzpcl2  42741  mzpf  42747  mzpadd  42749  mzpmul  42750  mzpsubmpt  42754  mzpnegmpt  42755  mzpexpmpt  42756  mzpindd  42757  mzpsubst  42759  mzpcompact2  42763  mzpcong  42984  sprel  47471  grtriprop  47908  clintop  48124  assintop  48125  clintopcllaw  48127  assintopcllaw  48128  assintopass  48130