Theorem elfvex 6939

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

Syntax hints:   → wi 4   ∈ wcel 2099  Vcvv 3462  dom cdm 5682  ‘cfv 6554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-nul 5311  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-dm 5692  df-iota 6506  df-fv 6562

This theorem is referenced by:  elfvexd  6940  fviss  6979  fiin  9465  elharval  9604  elfzp12  13634  ismre  17603  ismri  17644  isacs  17664  oppccofval  17730  mulgnngsum  19073  gexid  19579  efgrcl  19713  islss  20911  thlle  21694  thlleOLD  21695  islbs4  21830  istopon  22905  fgval  23865  fgcl  23873  ufilen  23925  ustssxp  24200  ustbasel  24202  ustincl  24203  ustdiag  24204  ustinvel  24205  ustexhalf  24206  ustfilxp  24208  ustbas2  24221  trust  24225  utopval  24228  elutop  24229  restutop  24233  ustuqtop5  24241  isucn  24274  psmetdmdm  24302  psmetf  24303  psmet0  24305  psmettri2  24306  psmetres2  24311  ismet2  24330  xmetpsmet  24345  metustfbas  24557  metust  24558  iscmet  25303  ulmscl  26408  1vgrex  28938  wlkcompim  29569  clwlkcompim  29717  wwlkbp  29775  2wlkdlem7  29866  clwwlkbp  29918  3wlkdlem7  30099  metidval  33705  pstmval  33710  pstmxmet  33712  issiga  33945  insiga  33970  mvrsval  35333  mrsubcv  35338  mrsubccat  35346  mppsval  35400  topdifinffinlem  37054  istotbnd  37470  isbnd  37481  ismrc  42358  isnacs  42361  mzpcl1  42386  mzpcl2  42387  mzpf  42393  mzpadd  42395  mzpmul  42396  mzpsubmpt  42400  mzpnegmpt  42401  mzpexpmpt  42402  mzpindd  42403  mzpsubst  42405  mzpcompact2  42409  mzpcong  42630  sprel  47056  clintop  47585  assintop  47586  clintopcllaw  47588  assintopcllaw  47589  assintopass  47591