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

Syntax hints:   → wi 4   ∈ wcel 2141  Vcvv 3453  dom cdm 5661  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5268  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3415  df-v 3455  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 5671  df-iota 6492  df-fv 6544

This theorem is referenced by:  elfvexd  6917  fviss  6958  fiin  9381  elharval  9522  elfzp12  13631  ismre  17641  ismri  17686  isacs  17706  oppccofval  17771  mulgnngsum  19144  gexid  19650  efgrcl  19784  islss  21034  thlle  21826  islbs4  21961  istopon  23048  fgval  24006  fgcl  24014  ufilen  24066  ustssxp  24341  ustbasel  24343  ustincl  24344  ustdiag  24345  ustinvel  24346  ustexhalf  24347  ustfilxp  24349  ustbas2  24361  trust  24365  utopval  24368  elutop  24369  restutop  24373  ustuqtop5  24381  isucn  24413  psmetdmdm  24441  psmetf  24442  psmet0  24444  psmettri2  24445  psmetres2  24450  ismet2  24469  xmetpsmet  24484  metustfbas  24693  metust  24694  iscmet  25422  ulmscl  26518  1vgrex  29318  wlkcompim  29947  clwlkcompim  30095  wwlkbp  30156  2wlkdlem7  30247  clwwlkbp  30302  3wlkdlem7  30483  metidval  34246  pstmval  34251  pstmxmet  34253  issiga  34468  insiga  34493  mvrsval  35963  mrsubcv  35968  mrsubccat  35976  mppsval  36030  topdifinffinlem  37959  istotbnd  38386  isbnd  38397  ismrc  43402  isnacs  43405  mzpcl1  43430  mzpcl2  43431  mzpf  43437  mzpadd  43439  mzpmul  43440  mzpsubmpt  43444  mzpnegmpt  43445  mzpexpmpt  43446  mzpindd  43447  mzpsubst  43449  mzpcompact2  43453  mzpcong  43669  sprel  48200  grtriprop  48673  clintop  48940  assintop  48941  clintopcllaw  48943  assintopcllaw  48944  assintopass  48946  oppcinito  49980  oppctermo  49981  oppczeroo  49982