Theorem elfvex 6571

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

Syntax hints:   → wi 4   ∈ wcel 2081  Vcvv 3437  dom cdm 5443  ‘cfv 6225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-nul 5101  ax-pow 5157

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-dm 5453  df-iota 6189  df-fv 6233

This theorem is referenced by:  elfvexd  6572  fviss  6608  fiin  8732  elharval  8873  elfzp12  12836  ismre  16690  ismri  16731  isacs  16751  oppccofval  16815  gexid  18436  efgrcl  18568  islss  19396  thlle  20523  islbs4  20658  istopon  21204  fgval  22162  fgcl  22170  ufilen  22222  ustssxp  22496  ustbasel  22498  ustincl  22499  ustdiag  22500  ustinvel  22501  ustexhalf  22502  ustfilxp  22504  ustbas2  22517  trust  22521  utopval  22524  elutop  22525  restutop  22529  ustuqtop5  22537  isucn  22570  psmetdmdm  22598  psmetf  22599  psmet0  22601  psmettri2  22602  psmetres2  22607  ismet2  22626  xmetpsmet  22641  metustfbas  22850  metust  22851  iscmet  23570  ulmscl  24650  1vgrex  26470  wlkcompim  27096  clwlkcompim  27248  wwlkbp  27306  2wlkdlem7  27398  clwwlkbp  27450  3wlkdlem7  27632  metidval  30747  pstmval  30752  pstmxmet  30754  issiga  30988  insiga  31013  mvrsval  32361  mrsubcv  32366  mrsubccat  32374  mppsval  32428  topdifinffinlem  34178  istotbnd  34598  isbnd  34609  ismrc  38802  isnacs  38805  mzpcl1  38830  mzpcl2  38831  mzpf  38837  mzpadd  38839  mzpmul  38840  mzpsubmpt  38844  mzpnegmpt  38845  mzpexpmpt  38846  mzpindd  38847  mzpsubst  38849  mzpcompact2  38853  mzpcong  39073  sprel  43148  clintop  43613  assintop  43614  clintopcllaw  43616  assintopcllaw  43617  assintopass  43619