Theorem elfvex 6896

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447  dom cdm 5638  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-dm 5648  df-iota 6464  df-fv 6519

This theorem is referenced by:  elfvexd  6897  fviss  6938  fiin  9373  elharval  9514  elfzp12  13564  ismre  17551  ismri  17592  isacs  17612  oppccofval  17677  mulgnngsum  19011  gexid  19511  efgrcl  19645  islss  20840  thlle  21606  islbs4  21741  istopon  22799  fgval  23757  fgcl  23765  ufilen  23817  ustssxp  24092  ustbasel  24094  ustincl  24095  ustdiag  24096  ustinvel  24097  ustexhalf  24098  ustfilxp  24100  ustbas2  24113  trust  24117  utopval  24120  elutop  24121  restutop  24125  ustuqtop5  24133  isucn  24165  psmetdmdm  24193  psmetf  24194  psmet0  24196  psmettri2  24197  psmetres2  24202  ismet2  24221  xmetpsmet  24236  metustfbas  24445  metust  24446  iscmet  25184  ulmscl  26288  1vgrex  28929  wlkcompim  29560  clwlkcompim  29710  wwlkbp  29771  2wlkdlem7  29862  clwwlkbp  29914  3wlkdlem7  30095  metidval  33880  pstmval  33885  pstmxmet  33887  issiga  34102  insiga  34127  mvrsval  35492  mrsubcv  35497  mrsubccat  35505  mppsval  35559  topdifinffinlem  37335  istotbnd  37763  isbnd  37774  ismrc  42689  isnacs  42692  mzpcl1  42717  mzpcl2  42718  mzpf  42724  mzpadd  42726  mzpmul  42727  mzpsubmpt  42731  mzpnegmpt  42732  mzpexpmpt  42733  mzpindd  42734  mzpsubst  42736  mzpcompact2  42740  mzpcong  42961  sprel  47485  grtriprop  47940  clintop  48196  assintop  48197  clintopcllaw  48199  assintopcllaw  48200  assintopass  48202  oppcinito  49224  oppctermo  49225  oppczeroo  49226