Theorem elfvex 6221

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 6220	. 2 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹)
2		elex 3212	. 2 ⊢ (𝐵 ∈ dom 𝐹 → 𝐵 ∈ V)
3	1, 2	syl 17	1 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 1990  Vcvv 3200  dom cdm 5114  ‘cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789  ax-pow 4843

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-dm 5124  df-iota 5851  df-fv 5896

This theorem is referenced by:  elfvexd  6222  fviss  6256  fiin  8328  elharval  8468  elfzp12  12419  ismre  16250  ismri  16291  isacs  16312  oppccofval  16376  gexid  17996  efgrcl  18128  islss  18935  thlle  20041  islbs4  20171  istopon  20717  fgval  21674  fgcl  21682  ufilen  21734  ustssxp  22008  ustbasel  22010  ustincl  22011  ustdiag  22012  ustinvel  22013  ustexhalf  22014  ustfilxp  22016  ustbas2  22029  trust  22033  utopval  22036  elutop  22037  restutop  22041  ustuqtop5  22049  isucn  22082  psmetdmdm  22110  psmetf  22111  psmet0  22113  psmettri2  22114  psmetres2  22119  ismet2  22138  xmetpsmet  22153  metustfbas  22362  metust  22363  iscmet  23082  ulmscl  24133  1vgrex  25882  uvtxaisvtx  26289  vtxnbuvtx  26291  uvtxanbgrvtx  26293  uvtxnbgr  26301  wlkcompim  26527  clwlkcompim  26676  wwlkbp  26732  2wlkdlem7  26828  clwwlkbp  26883  3wlkdlem7  27026  metidval  29933  pstmval  29938  pstmxmet  29940  issiga  30174  insiga  30200  mvrsval  31402  mrsubcv  31407  mrsubccat  31415  mppsval  31469  topdifinffinlem  33195  istotbnd  33568  isbnd  33579  ismrc  37264  isnacs  37267  mzpcl1  37292  mzpcl2  37293  mzpf  37299  mzpadd  37301  mzpmul  37302  mzpsubmpt  37306  mzpnegmpt  37307  mzpexpmpt  37308  mzpindd  37309  mzpsubst  37311  mzpcompact2  37315  mzpcong  37539  sprel  41734  clintop  41844  assintop  41845  clintopcllaw  41847  assintopcllaw  41848  assintopass  41850