Theorem elfvex 6891

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

Syntax hints:   → wi 4   ∈ wcel 2136  Vcvv 3448  dom cdm 5640  ‘cfv 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-nul 5250  ax-pr 5384

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-ne 2952  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-dm 5650  df-iota 6466  df-fv 6518

This theorem is referenced by:  elfvexd  6892  fviss  6933  fiin  9358  elharval  9499  elfzp12  13598  ismre  17594  ismri  17639  isacs  17659  oppccofval  17724  mulgnngsum  19097  gexid  19597  efgrcl  19731  islss  20974  thlle  21722  islbs4  21857  istopon  22945  fgval  23903  fgcl  23911  ufilen  23963  ustssxp  24238  ustbasel  24240  ustincl  24241  ustdiag  24242  ustinvel  24243  ustexhalf  24244  ustfilxp  24246  ustbas2  24258  trust  24262  utopval  24265  elutop  24266  restutop  24270  ustuqtop5  24278  isucn  24310  psmetdmdm  24338  psmetf  24339  psmet0  24341  psmettri2  24342  psmetres2  24347  ismet2  24366  xmetpsmet  24381  metustfbas  24590  metust  24591  iscmet  25319  ulmscl  26412  1vgrex  29142  wlkcompim  29771  clwlkcompim  29919  wwlkbp  29980  2wlkdlem7  30071  clwwlkbp  30126  3wlkdlem7  30307  metidval  34141  pstmval  34146  pstmxmet  34148  issiga  34363  insiga  34388  mvrsval  35803  mrsubcv  35808  mrsubccat  35816  mppsval  35870  topdifinffinlem  37789  istotbnd  38216  isbnd  38227  ismrc  43230  isnacs  43233  mzpcl1  43258  mzpcl2  43259  mzpf  43265  mzpadd  43267  mzpmul  43268  mzpsubmpt  43272  mzpnegmpt  43273  mzpexpmpt  43274  mzpindd  43275  mzpsubst  43277  mzpcompact2  43281  mzpcong  43497  sprel  48038  grtriprop  48511  clintop  48778  assintop  48779  clintopcllaw  48781  assintopcllaw  48782  assintopass  48784  oppcinito  49804  oppctermo  49805  oppczeroo  49806