Theorem elfvex 6898

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450  dom cdm 5640  ‘cfv 6513

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 5263  ax-pr 5389

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 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-dm 5650  df-iota 6466  df-fv 6521

This theorem is referenced by:  elfvexd  6899  fviss  6940  fiin  9379  elharval  9520  elfzp12  13570  ismre  17557  ismri  17598  isacs  17618  oppccofval  17683  mulgnngsum  19017  gexid  19517  efgrcl  19651  islss  20846  thlle  21612  islbs4  21747  istopon  22805  fgval  23763  fgcl  23771  ufilen  23823  ustssxp  24098  ustbasel  24100  ustincl  24101  ustdiag  24102  ustinvel  24103  ustexhalf  24104  ustfilxp  24106  ustbas2  24119  trust  24123  utopval  24126  elutop  24127  restutop  24131  ustuqtop5  24139  isucn  24171  psmetdmdm  24199  psmetf  24200  psmet0  24202  psmettri2  24203  psmetres2  24208  ismet2  24227  xmetpsmet  24242  metustfbas  24451  metust  24452  iscmet  25190  ulmscl  26294  1vgrex  28935  wlkcompim  29566  clwlkcompim  29716  wwlkbp  29777  2wlkdlem7  29868  clwwlkbp  29920  3wlkdlem7  30101  metidval  33886  pstmval  33891  pstmxmet  33893  issiga  34108  insiga  34133  mvrsval  35492  mrsubcv  35497  mrsubccat  35505  mppsval  35559  topdifinffinlem  37330  istotbnd  37758  isbnd  37769  ismrc  42682  isnacs  42685  mzpcl1  42710  mzpcl2  42711  mzpf  42717  mzpadd  42719  mzpmul  42720  mzpsubmpt  42724  mzpnegmpt  42725  mzpexpmpt  42726  mzpindd  42727  mzpsubst  42729  mzpcompact2  42733  mzpcong  42954  sprel  47475  grtriprop  47930  clintop  48186  assintop  48187  clintopcllaw  48189  assintopcllaw  48190  assintopass  48192  oppcinito  49214  oppctermo  49215  oppczeroo  49216