Theorem elfvex 6877

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442  dom cdm 5632  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-dm 5642  df-iota 6456  df-fv 6508

This theorem is referenced by:  elfvexd  6878  fviss  6919  fiin  9337  elharval  9478  elfzp12  13531  ismre  17521  ismri  17566  isacs  17586  oppccofval  17651  mulgnngsum  19021  gexid  19522  efgrcl  19656  islss  20897  thlle  21664  islbs4  21799  istopon  22868  fgval  23826  fgcl  23834  ufilen  23886  ustssxp  24161  ustbasel  24163  ustincl  24164  ustdiag  24165  ustinvel  24166  ustexhalf  24167  ustfilxp  24169  ustbas2  24181  trust  24185  utopval  24188  elutop  24189  restutop  24193  ustuqtop5  24201  isucn  24233  psmetdmdm  24261  psmetf  24262  psmet0  24264  psmettri2  24265  psmetres2  24270  ismet2  24289  xmetpsmet  24304  metustfbas  24513  metust  24514  iscmet  25252  ulmscl  26356  1vgrex  29087  wlkcompim  29717  clwlkcompim  29865  wwlkbp  29926  2wlkdlem7  30017  clwwlkbp  30072  3wlkdlem7  30253  metidval  34067  pstmval  34072  pstmxmet  34074  issiga  34289  insiga  34314  mvrsval  35718  mrsubcv  35723  mrsubccat  35731  mppsval  35785  topdifinffinlem  37591  istotbnd  38009  isbnd  38020  ismrc  43047  isnacs  43050  mzpcl1  43075  mzpcl2  43076  mzpf  43082  mzpadd  43084  mzpmul  43085  mzpsubmpt  43089  mzpnegmpt  43090  mzpexpmpt  43091  mzpindd  43092  mzpsubst  43094  mzpcompact2  43098  mzpcong  43318  sprel  47833  grtriprop  48290  clintop  48557  assintop  48558  clintopcllaw  48560  assintopcllaw  48561  assintopass  48563  oppcinito  49583  oppctermo  49584  oppczeroo  49585