Theorem elfvex 6852

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

Syntax hints:   → wi 4   ∈ wcel 2110  Vcvv 3434  dom cdm 5614  ‘cfv 6477

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 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-dm 5624  df-iota 6433  df-fv 6485

This theorem is referenced by:  elfvexd  6853  fviss  6894  fiin  9301  elharval  9442  elfzp12  13495  ismre  17484  ismri  17529  isacs  17549  oppccofval  17614  mulgnngsum  18984  gexid  19486  efgrcl  19620  islss  20860  thlle  21627  islbs4  21762  istopon  22820  fgval  23778  fgcl  23786  ufilen  23838  ustssxp  24113  ustbasel  24115  ustincl  24116  ustdiag  24117  ustinvel  24118  ustexhalf  24119  ustfilxp  24121  ustbas2  24133  trust  24137  utopval  24140  elutop  24141  restutop  24145  ustuqtop5  24153  isucn  24185  psmetdmdm  24213  psmetf  24214  psmet0  24216  psmettri2  24217  psmetres2  24222  ismet2  24241  xmetpsmet  24256  metustfbas  24465  metust  24466  iscmet  25204  ulmscl  26308  1vgrex  28973  wlkcompim  29603  clwlkcompim  29751  wwlkbp  29812  2wlkdlem7  29903  clwwlkbp  29955  3wlkdlem7  30136  metidval  33893  pstmval  33898  pstmxmet  33900  issiga  34115  insiga  34140  mvrsval  35517  mrsubcv  35522  mrsubccat  35530  mppsval  35584  topdifinffinlem  37360  istotbnd  37788  isbnd  37799  ismrc  42713  isnacs  42716  mzpcl1  42741  mzpcl2  42742  mzpf  42748  mzpadd  42750  mzpmul  42751  mzpsubmpt  42755  mzpnegmpt  42756  mzpexpmpt  42757  mzpindd  42758  mzpsubst  42760  mzpcompact2  42764  mzpcong  42984  sprel  47494  grtriprop  47951  clintop  48218  assintop  48219  clintopcllaw  48221  assintopcllaw  48222  assintopass  48224  oppcinito  49246  oppctermo  49247  oppczeroo  49248