Theorem elfvex 6807

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3432  dom cdm 5589  ‘cfv 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-dm 5599  df-iota 6391  df-fv 6441

This theorem is referenced by:  elfvexd  6808  fviss  6845  fiin  9181  elharval  9320  elfzp12  13335  ismre  17299  ismri  17340  isacs  17360  oppccofval  17426  mulgnngsum  18709  gexid  19186  efgrcl  19321  islss  20196  thlle  20903  thlleOLD  20904  islbs4  21039  istopon  22061  fgval  23021  fgcl  23029  ufilen  23081  ustssxp  23356  ustbasel  23358  ustincl  23359  ustdiag  23360  ustinvel  23361  ustexhalf  23362  ustfilxp  23364  ustbas2  23377  trust  23381  utopval  23384  elutop  23385  restutop  23389  ustuqtop5  23397  isucn  23430  psmetdmdm  23458  psmetf  23459  psmet0  23461  psmettri2  23462  psmetres2  23467  ismet2  23486  xmetpsmet  23501  metustfbas  23713  metust  23714  iscmet  24448  ulmscl  25538  1vgrex  27372  wlkcompim  27999  clwlkcompim  28148  wwlkbp  28206  2wlkdlem7  28297  clwwlkbp  28349  3wlkdlem7  28530  metidval  31840  pstmval  31845  pstmxmet  31847  issiga  32080  insiga  32105  mvrsval  33467  mrsubcv  33472  mrsubccat  33480  mppsval  33534  topdifinffinlem  35518  istotbnd  35927  isbnd  35938  ismrc  40523  isnacs  40526  mzpcl1  40551  mzpcl2  40552  mzpf  40558  mzpadd  40560  mzpmul  40561  mzpsubmpt  40565  mzpnegmpt  40566  mzpexpmpt  40567  mzpindd  40568  mzpsubst  40570  mzpcompact2  40574  mzpcong  40794  sprel  44936  clintop  45402  assintop  45403  clintopcllaw  45405  assintopcllaw  45406  assintopass  45408