Theorem elfvex 6885

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3446  dom cdm 5638  ‘cfv 6501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-dm 5648  df-iota 6453  df-fv 6509

This theorem is referenced by:  elfvexd  6886  fviss  6923  fiin  9367  elharval  9506  elfzp12  13530  ismre  17484  ismri  17525  isacs  17545  oppccofval  17611  mulgnngsum  18895  gexid  19377  efgrcl  19511  islss  20452  thlle  21139  thlleOLD  21140  islbs4  21275  istopon  22298  fgval  23258  fgcl  23266  ufilen  23318  ustssxp  23593  ustbasel  23595  ustincl  23596  ustdiag  23597  ustinvel  23598  ustexhalf  23599  ustfilxp  23601  ustbas2  23614  trust  23618  utopval  23621  elutop  23622  restutop  23626  ustuqtop5  23634  isucn  23667  psmetdmdm  23695  psmetf  23696  psmet0  23698  psmettri2  23699  psmetres2  23704  ismet2  23723  xmetpsmet  23738  metustfbas  23950  metust  23951  iscmet  24685  ulmscl  25775  1vgrex  28016  wlkcompim  28643  clwlkcompim  28791  wwlkbp  28849  2wlkdlem7  28940  clwwlkbp  28992  3wlkdlem7  29173  metidval  32560  pstmval  32565  pstmxmet  32567  issiga  32800  insiga  32825  mvrsval  34186  mrsubcv  34191  mrsubccat  34199  mppsval  34253  topdifinffinlem  35891  istotbnd  36301  isbnd  36312  ismrc  41082  isnacs  41085  mzpcl1  41110  mzpcl2  41111  mzpf  41117  mzpadd  41119  mzpmul  41120  mzpsubmpt  41124  mzpnegmpt  41125  mzpexpmpt  41126  mzpindd  41127  mzpsubst  41129  mzpcompact2  41133  mzpcong  41354  sprel  45796  clintop  46262  assintop  46263  clintopcllaw  46265  assintopcllaw  46266  assintopass  46268