Theorem elfvex 6906

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

Syntax hints:   → wi 4   ∈ wcel 2145  Vcvv 3457  dom cdm 5652  ‘cfv 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-dm 5662  df-iota 6481  df-fv 6533

This theorem is referenced by:  elfvexd  6907  fviss  6948  fiin  9370  elharval  9511  elfzp12  13622  ismre  17632  ismri  17677  isacs  17697  oppccofval  17762  mulgnngsum  19136  gexid  19642  efgrcl  19776  islss  21024  thlle  21807  islbs4  21942  istopon  23030  fgval  23988  fgcl  23996  ufilen  24048  ustssxp  24323  ustbasel  24325  ustincl  24326  ustdiag  24327  ustinvel  24328  ustexhalf  24329  ustfilxp  24331  ustbas2  24343  trust  24347  utopval  24350  elutop  24351  restutop  24355  ustuqtop5  24363  isucn  24395  psmetdmdm  24423  psmetf  24424  psmet0  24426  psmettri2  24427  psmetres2  24432  ismet2  24451  xmetpsmet  24466  metustfbas  24675  metust  24676  iscmet  25404  ulmscl  26500  1vgrex  29261  wlkcompim  29890  clwlkcompim  30038  wwlkbp  30099  2wlkdlem7  30190  clwwlkbp  30245  3wlkdlem7  30426  metidval  34197  pstmval  34202  pstmxmet  34204  issiga  34419  insiga  34444  mvrsval  35868  mrsubcv  35873  mrsubccat  35881  mppsval  35935  topdifinffinlem  37853  istotbnd  38280  isbnd  38291  ismrc  43294  isnacs  43297  mzpcl1  43322  mzpcl2  43323  mzpf  43329  mzpadd  43331  mzpmul  43332  mzpsubmpt  43336  mzpnegmpt  43337  mzpexpmpt  43338  mzpindd  43339  mzpsubst  43341  mzpcompact2  43345  mzpcong  43561  sprel  48088  grtriprop  48561  clintop  48828  assintop  48829  clintopcllaw  48831  assintopcllaw  48832  assintopass  48834  oppcinito  49864  oppctermo  49865  oppczeroo  49866