Theorem elfvex 6899

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450  dom cdm 5641  ‘cfv 6514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-dm 5651  df-iota 6467  df-fv 6522

This theorem is referenced by:  elfvexd  6900  fviss  6941  fiin  9380  elharval  9521  elfzp12  13571  ismre  17558  ismri  17599  isacs  17619  oppccofval  17684  mulgnngsum  19018  gexid  19518  efgrcl  19652  islss  20847  thlle  21613  islbs4  21748  istopon  22806  fgval  23764  fgcl  23772  ufilen  23824  ustssxp  24099  ustbasel  24101  ustincl  24102  ustdiag  24103  ustinvel  24104  ustexhalf  24105  ustfilxp  24107  ustbas2  24120  trust  24124  utopval  24127  elutop  24128  restutop  24132  ustuqtop5  24140  isucn  24172  psmetdmdm  24200  psmetf  24201  psmet0  24203  psmettri2  24204  psmetres2  24209  ismet2  24228  xmetpsmet  24243  metustfbas  24452  metust  24453  iscmet  25191  ulmscl  26295  1vgrex  28936  wlkcompim  29567  clwlkcompim  29717  wwlkbp  29778  2wlkdlem7  29869  clwwlkbp  29921  3wlkdlem7  30102  metidval  33887  pstmval  33892  pstmxmet  33894  issiga  34109  insiga  34134  mvrsval  35499  mrsubcv  35504  mrsubccat  35512  mppsval  35566  topdifinffinlem  37342  istotbnd  37770  isbnd  37781  ismrc  42696  isnacs  42699  mzpcl1  42724  mzpcl2  42725  mzpf  42731  mzpadd  42733  mzpmul  42734  mzpsubmpt  42738  mzpnegmpt  42739  mzpexpmpt  42740  mzpindd  42741  mzpsubst  42743  mzpcompact2  42747  mzpcong  42968  sprel  47489  grtriprop  47944  clintop  48200  assintop  48201  clintopcllaw  48203  assintopcllaw  48204  assintopass  48206  oppcinito  49228  oppctermo  49229  oppczeroo  49230