Theorem elfvex 6943

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Vcvv 3454  dom cdm 5655  ‘cfv 6558

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-dm 5665  df-iota 6512  df-fv 6566

This theorem is used by:  elfvexd  6944  fviss  6985  fiin  9441  elharval  9582  elfzp12  13764  ismre  17789  ismri  17834  isacs  17854  oppccofval  17919  mulgnngsum  19318  gexid  19825  efgrcl  19959  islss  21239  thlle  22033  islbs4  22168  istopon  23260  fgval  24219  fgcl  24227  ufilen  24279  ustssxp  24554  ustbasel  24556  ustincl  24557  ustdiag  24558  ustinvel  24559  ustexhalf  24560  ustfilxp  24562  ustbas2  24574  trust  24578  utopval  24581  elutop  24582  restutop  24586  ustuqtop5  24594  isucn  24626  psmetdmdm  24654  psmetf  24655  psmet0  24657  psmettri2  24658  psmetres2  24663  ismet2  24682  xmetpsmet  24697  metustfbas  24906  metust  24907  iscmet  25635  ulmscl  26736  1vgrex  29610  wlkcompim  30242  clwlkcompim  30397  wwlkbp  30460  2wlkdlem7  30551  clwwlkbp  30606  3wlkdlem7  30797  metidval  34592  pstmval  34597  pstmxmet  34599  issiga  34814  insiga  34840  mvrsval  36437  mrsubcv  36442  mrsubccat  36450  mppsval  36504  topdifinffinlem  38462  istotbnd  38895  isbnd  38906  ismrc  43905  isnacs  43908  mzpcl1  43933  mzpcl2  43934  mzpf  43940  mzpadd  43942  mzpmul  43943  mzpsubmpt  43947  mzpnegmpt  43948  mzpexpmpt  43949  mzpindd  43950  mzpsubst  43952  mzpcompact2  43956  mzpcong  44172  sprel  48771  grtriprop  49244  clintop  49510  assintop  49511  clintopcllaw  49513  assintopcllaw  49514  assintopass  49516  oppcinito  50562  oppctermo  50563  oppczeroo  50564