Theorem elfvex 6920

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450  dom cdm 5650  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-dm 5660  df-iota 6494  df-fv 6546

This theorem is used by:  elfvexd  6921  fviss  6962  fiin  9415  elharval  9556  elfzp12  13738  ismre  17761  ismri  17806  isacs  17826  oppccofval  17891  mulgnngsum  19290  gexid  19796  efgrcl  19930  islss  21210  thlle  22004  islbs4  22139  istopon  23231  fgval  24190  fgcl  24198  ufilen  24250  ustssxp  24525  ustbasel  24527  ustincl  24528  ustdiag  24529  ustinvel  24530  ustexhalf  24531  ustfilxp  24533  ustbas2  24545  trust  24549  utopval  24552  elutop  24553  restutop  24557  ustuqtop5  24565  isucn  24597  psmetdmdm  24625  psmetf  24626  psmet0  24628  psmettri2  24629  psmetres2  24634  ismet2  24653  xmetpsmet  24668  metustfbas  24877  metust  24878  iscmet  25606  ulmscl  26707  1vgrex  29581  wlkcompim  30213  clwlkcompim  30368  wwlkbp  30431  2wlkdlem7  30522  clwwlkbp  30577  3wlkdlem7  30768  metidval  34565  pstmval  34570  pstmxmet  34572  issiga  34787  insiga  34813  mvrsval  36339  mrsubcv  36344  mrsubccat  36352  mppsval  36406  topdifinffinlem  38346  istotbnd  38779  isbnd  38790  ismrc  43788  isnacs  43791  mzpcl1  43816  mzpcl2  43817  mzpf  43823  mzpadd  43825  mzpmul  43826  mzpsubmpt  43830  mzpnegmpt  43831  mzpexpmpt  43832  mzpindd  43833  mzpsubst  43835  mzpcompact2  43839  mzpcong  44055  sprel  48642  grtriprop  49115  clintop  49381  assintop  49382  clintopcllaw  49384  assintopcllaw  49385  assintopass  49387  oppcinito  50419  oppctermo  50420  oppczeroo  50421