Theorem elfvex 6917

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3453  dom cdm 5659  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-dm 5669  df-iota 6493  df-fv 6545

This theorem is used by:  elfvexd  6918  fviss  6959  fiin  9395  elharval  9536  elfzp12  13660  ismre  17678  ismri  17723  isacs  17743  oppccofval  17808  mulgnngsum  19206  gexid  19712  efgrcl  19846  islss  21122  thlle  21914  islbs4  22049  istopon  23141  fgval  24100  fgcl  24108  ufilen  24160  ustssxp  24435  ustbasel  24437  ustincl  24438  ustdiag  24439  ustinvel  24440  ustexhalf  24441  ustfilxp  24443  ustbas2  24455  trust  24459  utopval  24462  elutop  24463  restutop  24467  ustuqtop5  24475  isucn  24507  psmetdmdm  24535  psmetf  24536  psmet0  24538  psmettri2  24539  psmetres2  24544  ismet2  24563  xmetpsmet  24578  metustfbas  24787  metust  24788  iscmet  25516  ulmscl  26615  1vgrex  29460  wlkcompim  30092  clwlkcompim  30247  wwlkbp  30310  2wlkdlem7  30401  clwwlkbp  30456  3wlkdlem7  30647  metidval  34402  pstmval  34407  pstmxmet  34409  issiga  34624  insiga  34650  mvrsval  36086  mrsubcv  36091  mrsubccat  36099  mppsval  36153  topdifinffinlem  38103  istotbnd  38521  isbnd  38532  ismrc  43548  isnacs  43551  mzpcl1  43576  mzpcl2  43577  mzpf  43583  mzpadd  43585  mzpmul  43586  mzpsubmpt  43590  mzpnegmpt  43591  mzpexpmpt  43592  mzpindd  43593  mzpsubst  43595  mzpcompact2  43599  mzpcong  43815  sprel  48386  grtriprop  48859  clintop  49125  assintop  49126  clintopcllaw  49128  assintopcllaw  49129  assintopass  49131  oppcinito  50163  oppctermo  50164  oppczeroo  50165