Theorem elfvex 6728

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

Syntax hints:   → wi 4   ∈ wcel 2112  Vcvv 3398  dom cdm 5536  ‘cfv 6358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-dm 5546  df-iota 6316  df-fv 6366

This theorem is referenced by:  elfvexd  6729  fviss  6766  fiin  9016  elharval  9155  elfzp12  13156  ismre  17047  ismri  17088  isacs  17108  oppccofval  17174  mulgnngsum  18451  gexid  18924  efgrcl  19059  islss  19925  thlle  20613  islbs4  20748  istopon  21763  fgval  22721  fgcl  22729  ufilen  22781  ustssxp  23056  ustbasel  23058  ustincl  23059  ustdiag  23060  ustinvel  23061  ustexhalf  23062  ustfilxp  23064  ustbas2  23077  trust  23081  utopval  23084  elutop  23085  restutop  23089  ustuqtop5  23097  isucn  23129  psmetdmdm  23157  psmetf  23158  psmet0  23160  psmettri2  23161  psmetres2  23166  ismet2  23185  xmetpsmet  23200  metustfbas  23409  metust  23410  iscmet  24135  ulmscl  25225  1vgrex  27047  wlkcompim  27673  clwlkcompim  27821  wwlkbp  27879  2wlkdlem7  27970  clwwlkbp  28022  3wlkdlem7  28203  metidval  31508  pstmval  31513  pstmxmet  31515  issiga  31746  insiga  31771  mvrsval  33134  mrsubcv  33139  mrsubccat  33147  mppsval  33201  topdifinffinlem  35204  istotbnd  35613  isbnd  35624  ismrc  40167  isnacs  40170  mzpcl1  40195  mzpcl2  40196  mzpf  40202  mzpadd  40204  mzpmul  40205  mzpsubmpt  40209  mzpnegmpt  40210  mzpexpmpt  40211  mzpindd  40212  mzpsubst  40214  mzpcompact2  40218  mzpcong  40438  sprel  44552  clintop  45018  assintop  45019  clintopcllaw  45021  assintopcllaw  45022  assintopass  45024