Theorem elfvex 6875

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429  dom cdm 5631  ‘cfv 6498

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-dm 5641  df-iota 6454  df-fv 6506

This theorem is referenced by:  elfvexd  6876  fviss  6917  fiin  9335  elharval  9476  elfzp12  13557  ismre  17552  ismri  17597  isacs  17617  oppccofval  17682  mulgnngsum  19055  gexid  19556  efgrcl  19690  islss  20929  thlle  21677  islbs4  21812  istopon  22877  fgval  23835  fgcl  23843  ufilen  23895  ustssxp  24170  ustbasel  24172  ustincl  24173  ustdiag  24174  ustinvel  24175  ustexhalf  24176  ustfilxp  24178  ustbas2  24190  trust  24194  utopval  24197  elutop  24198  restutop  24202  ustuqtop5  24210  isucn  24242  psmetdmdm  24270  psmetf  24271  psmet0  24273  psmettri2  24274  psmetres2  24279  ismet2  24298  xmetpsmet  24313  metustfbas  24522  metust  24523  iscmet  25251  ulmscl  26344  1vgrex  29071  wlkcompim  29700  clwlkcompim  29848  wwlkbp  29909  2wlkdlem7  30000  clwwlkbp  30055  3wlkdlem7  30236  metidval  34034  pstmval  34039  pstmxmet  34041  issiga  34256  insiga  34281  mvrsval  35687  mrsubcv  35692  mrsubccat  35700  mppsval  35754  topdifinffinlem  37663  istotbnd  38090  isbnd  38101  ismrc  43133  isnacs  43136  mzpcl1  43161  mzpcl2  43162  mzpf  43168  mzpadd  43170  mzpmul  43171  mzpsubmpt  43175  mzpnegmpt  43176  mzpexpmpt  43177  mzpindd  43178  mzpsubst  43180  mzpcompact2  43184  mzpcong  43400  sprel  47944  grtriprop  48417  clintop  48684  assintop  48685  clintopcllaw  48687  assintopcllaw  48688  assintopass  48690  oppcinito  49710  oppctermo  49711  oppczeroo  49712