Theorem elfvex 6363

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

Syntax hints:   → wi 4   ∈ wcel 2145  Vcvv 3351  dom cdm 5250  ‘cfv 6032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-nul 4924  ax-pow 4975

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-dm 5260  df-iota 5995  df-fv 6040

This theorem is referenced by:  elfvexd  6364  fviss  6399  fiin  8485  elharval  8625  elfzp12  12627  ismre  16459  ismri  16500  isacs  16520  oppccofval  16584  gexid  18204  efgrcl  18336  islss  19146  thlle  20259  islbs4  20389  istopon  20938  fgval  21895  fgcl  21903  ufilen  21955  ustssxp  22229  ustbasel  22231  ustincl  22232  ustdiag  22233  ustinvel  22234  ustexhalf  22235  ustfilxp  22237  ustbas2  22250  trust  22254  utopval  22257  elutop  22258  restutop  22262  ustuqtop5  22270  isucn  22303  psmetdmdm  22331  psmetf  22332  psmet0  22334  psmettri2  22335  psmetres2  22340  ismet2  22359  xmetpsmet  22374  metustfbas  22583  metust  22584  iscmet  23302  ulmscl  24354  1vgrex  26104  wlkcompim  26763  clwlkcompim  26912  wwlkbp  26970  2wlkdlem7  27080  clwwlkbp  27136  3wlkdlem7  27347  metidval  30274  pstmval  30279  pstmxmet  30281  issiga  30515  insiga  30541  mvrsval  31741  mrsubcv  31746  mrsubccat  31754  mppsval  31808  topdifinffinlem  33533  istotbnd  33901  isbnd  33912  ismrc  37791  isnacs  37794  mzpcl1  37819  mzpcl2  37820  mzpf  37826  mzpadd  37828  mzpmul  37829  mzpsubmpt  37833  mzpnegmpt  37834  mzpexpmpt  37835  mzpindd  37836  mzpsubst  37838  mzpcompact2  37842  mzpcong  38066  sprel  42263  clintop  42373  assintop  42374  clintopcllaw  42376  assintopcllaw  42377  assintopass  42379