Theorem elfvex 6958

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488  dom cdm 5700  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-dm 5710  df-iota 6525  df-fv 6581

This theorem is referenced by:  elfvexd  6959  fviss  6999  fiin  9491  elharval  9630  elfzp12  13663  ismre  17648  ismri  17689  isacs  17709  oppccofval  17775  mulgnngsum  19119  gexid  19623  efgrcl  19757  islss  20955  thlle  21739  thlleOLD  21740  islbs4  21875  istopon  22939  fgval  23899  fgcl  23907  ufilen  23959  ustssxp  24234  ustbasel  24236  ustincl  24237  ustdiag  24238  ustinvel  24239  ustexhalf  24240  ustfilxp  24242  ustbas2  24255  trust  24259  utopval  24262  elutop  24263  restutop  24267  ustuqtop5  24275  isucn  24308  psmetdmdm  24336  psmetf  24337  psmet0  24339  psmettri2  24340  psmetres2  24345  ismet2  24364  xmetpsmet  24379  metustfbas  24591  metust  24592  iscmet  25337  ulmscl  26440  1vgrex  29037  wlkcompim  29668  clwlkcompim  29816  wwlkbp  29874  2wlkdlem7  29965  clwwlkbp  30017  3wlkdlem7  30198  metidval  33836  pstmval  33841  pstmxmet  33843  issiga  34076  insiga  34101  mvrsval  35473  mrsubcv  35478  mrsubccat  35486  mppsval  35540  topdifinffinlem  37313  istotbnd  37729  isbnd  37740  ismrc  42657  isnacs  42660  mzpcl1  42685  mzpcl2  42686  mzpf  42692  mzpadd  42694  mzpmul  42695  mzpsubmpt  42699  mzpnegmpt  42700  mzpexpmpt  42701  mzpindd  42702  mzpsubst  42704  mzpcompact2  42708  mzpcong  42929  sprel  47358  grtriprop  47792  clintop  47931  assintop  47932  clintopcllaw  47934  assintopcllaw  47935  assintopass  47937