Theorem elfvex 6334

Description: If a function value has a member, the argument is a set. (Contributed by Mario Carneiro, 6-Nov-2015.)

Assertion

Ref	Expression
elfvex	⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ V)

Proof of Theorem elfvex

Step	Hyp	Ref	Expression
1		elfvdm 6333	. 2 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹)
2		elex 3316	. 2 ⊢ (𝐵 ∈ dom 𝐹 → 𝐵 ∈ V)
3	1, 2	syl 17	1 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2103  Vcvv 3304  dom cdm 5218  ‘cfv 6001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-nul 4897  ax-pow 4948

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-dm 5228  df-iota 5964  df-fv 6009

This theorem is referenced by:  elfvexd  6335  fviss  6370  fiin  8444  elharval  8584  elfzp12  12533  ismre  16373  ismri  16414  isacs  16434  oppccofval  16498  gexid  18117  efgrcl  18249  islss  19058  thlle  20164  islbs4  20294  istopon  20840  fgval  21796  fgcl  21804  ufilen  21856  ustssxp  22130  ustbasel  22132  ustincl  22133  ustdiag  22134  ustinvel  22135  ustexhalf  22136  ustfilxp  22138  ustbas2  22151  trust  22155  utopval  22158  elutop  22159  restutop  22163  ustuqtop5  22171  isucn  22204  psmetdmdm  22232  psmetf  22233  psmet0  22235  psmettri2  22236  psmetres2  22241  ismet2  22260  xmetpsmet  22275  metustfbas  22484  metust  22485  iscmet  23203  ulmscl  24253  1vgrex  26002  wlkcompim  26658  clwlkcompim  26807  wwlkbp  26865  2wlkdlem7  26973  clwwlkbp  27029  3wlkdlem7  27239  metidval  30163  pstmval  30168  pstmxmet  30170  issiga  30404  insiga  30430  mvrsval  31630  mrsubcv  31635  mrsubccat  31643  mppsval  31697  topdifinffinlem  33427  istotbnd  33800  isbnd  33811  ismrc  37683  isnacs  37686  mzpcl1  37711  mzpcl2  37712  mzpf  37718  mzpadd  37720  mzpmul  37721  mzpsubmpt  37725  mzpnegmpt  37726  mzpexpmpt  37727  mzpindd  37728  mzpsubst  37730  mzpcompact2  37734  mzpcong  37958  sprel  42161  clintop  42271  assintop  42272  clintopcllaw  42274  assintopcllaw  42275  assintopass  42277