Theorem elfvex 6863

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3441  dom cdm 5620  ‘cfv 6479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-nul 5250  ax-pr 5372

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-dm 5630  df-iota 6431  df-fv 6487

This theorem is referenced by:  elfvexd  6864  fviss  6901  fiin  9279  elharval  9418  elfzp12  13436  ismre  17396  ismri  17437  isacs  17457  oppccofval  17523  mulgnngsum  18805  gexid  19282  efgrcl  19416  islss  20302  thlle  21009  thlleOLD  21010  islbs4  21145  istopon  22167  fgval  23127  fgcl  23135  ufilen  23187  ustssxp  23462  ustbasel  23464  ustincl  23465  ustdiag  23466  ustinvel  23467  ustexhalf  23468  ustfilxp  23470  ustbas2  23483  trust  23487  utopval  23490  elutop  23491  restutop  23495  ustuqtop5  23503  isucn  23536  psmetdmdm  23564  psmetf  23565  psmet0  23567  psmettri2  23568  psmetres2  23573  ismet2  23592  xmetpsmet  23607  metustfbas  23819  metust  23820  iscmet  24554  ulmscl  25644  1vgrex  27661  wlkcompim  28288  clwlkcompim  28436  wwlkbp  28494  2wlkdlem7  28585  clwwlkbp  28637  3wlkdlem7  28818  metidval  32138  pstmval  32143  pstmxmet  32145  issiga  32378  insiga  32403  mvrsval  33766  mrsubcv  33771  mrsubccat  33779  mppsval  33833  topdifinffinlem  35631  istotbnd  36040  isbnd  36051  ismrc  40793  isnacs  40796  mzpcl1  40821  mzpcl2  40822  mzpf  40828  mzpadd  40830  mzpmul  40831  mzpsubmpt  40835  mzpnegmpt  40836  mzpexpmpt  40837  mzpindd  40838  mzpsubst  40840  mzpcompact2  40844  mzpcong  41065  sprel  45295  clintop  45761  assintop  45762  clintopcllaw  45764  assintopcllaw  45765  assintopass  45767