Theorem elfvex 6916

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  Vcvv 3454  dom cdm 5660  ‘cfv 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5268  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-dm 5670  df-iota 6492  df-fv 6544

This theorem is used by:  elfvexd  6917  fviss  6958  fiin  9380  elharval  9521  elfzp12  13638  ismre  17648  ismri  17693  isacs  17713  oppccofval  17778  mulgnngsum  19151  gexid  19657  efgrcl  19791  islss  21066  thlle  21858  islbs4  21993  istopon  23080  fgval  24038  fgcl  24046  ufilen  24098  ustssxp  24373  ustbasel  24375  ustincl  24376  ustdiag  24377  ustinvel  24378  ustexhalf  24379  ustfilxp  24381  ustbas2  24393  trust  24397  utopval  24400  elutop  24401  restutop  24405  ustuqtop5  24413  isucn  24445  psmetdmdm  24473  psmetf  24474  psmet0  24476  psmettri2  24477  psmetres2  24482  ismet2  24501  xmetpsmet  24516  metustfbas  24725  metust  24726  iscmet  25454  ulmscl  26553  1vgrex  29363  wlkcompim  29992  clwlkcompim  30140  wwlkbp  30201  2wlkdlem7  30292  clwwlkbp  30347  3wlkdlem7  30528  metidval  34289  pstmval  34294  pstmxmet  34296  issiga  34511  insiga  34536  mvrsval  36005  mrsubcv  36010  mrsubccat  36018  mppsval  36072  topdifinffinlem  38021  istotbnd  38448  isbnd  38459  ismrc  43460  isnacs  43463  mzpcl1  43488  mzpcl2  43489  mzpf  43495  mzpadd  43497  mzpmul  43498  mzpsubmpt  43502  mzpnegmpt  43503  mzpexpmpt  43504  mzpindd  43505  mzpsubst  43507  mzpcompact2  43511  mzpcong  43727  sprel  48261  grtriprop  48734  clintop  49001  assintop  49002  clintopcllaw  49004  assintopcllaw  49005  assintopass  49007  oppcinito  50041  oppctermo  50042  oppczeroo  50043