Theorem elfvex 6945

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3478  dom cdm 5689  ‘cfv 6563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-dm 5699  df-iota 6516  df-fv 6571

This theorem is referenced by:  elfvexd  6946  fviss  6986  fiin  9460  elharval  9599  elfzp12  13640  ismre  17635  ismri  17676  isacs  17696  oppccofval  17762  mulgnngsum  19110  gexid  19614  efgrcl  19748  islss  20950  thlle  21734  thlleOLD  21735  islbs4  21870  istopon  22934  fgval  23894  fgcl  23902  ufilen  23954  ustssxp  24229  ustbasel  24231  ustincl  24232  ustdiag  24233  ustinvel  24234  ustexhalf  24235  ustfilxp  24237  ustbas2  24250  trust  24254  utopval  24257  elutop  24258  restutop  24262  ustuqtop5  24270  isucn  24303  psmetdmdm  24331  psmetf  24332  psmet0  24334  psmettri2  24335  psmetres2  24340  ismet2  24359  xmetpsmet  24374  metustfbas  24586  metust  24587  iscmet  25332  ulmscl  26437  1vgrex  29034  wlkcompim  29665  clwlkcompim  29813  wwlkbp  29871  2wlkdlem7  29962  clwwlkbp  30014  3wlkdlem7  30195  metidval  33851  pstmval  33856  pstmxmet  33858  issiga  34093  insiga  34118  mvrsval  35490  mrsubcv  35495  mrsubccat  35503  mppsval  35557  topdifinffinlem  37330  istotbnd  37756  isbnd  37767  ismrc  42689  isnacs  42692  mzpcl1  42717  mzpcl2  42718  mzpf  42724  mzpadd  42726  mzpmul  42727  mzpsubmpt  42731  mzpnegmpt  42732  mzpexpmpt  42733  mzpindd  42734  mzpsubst  42736  mzpcompact2  42740  mzpcong  42961  sprel  47409  grtriprop  47846  clintop  48052  assintop  48053  clintopcllaw  48055  assintopcllaw  48056  assintopass  48058