Theorem fex 3652

Description: If the domain of a mapping is a set, the function is a set.

Assertion

Ref	Expression
fex	|- ((F:A-->B /\ A e. C) -> F e. V)

Proof of Theorem fex

Step	Hyp	Ref	Expression
1		fnex 3607	. 2 |- ((F Fn A /\ A e. C) -> F e. V)
2		ffn 3627	. 2 |- (F:A-->B -> F Fn A)
3	1, 2	sylan 448	1 |- ((F:A-->B /\ A e. C) -> F e. V)

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 958  Vcvv 1811   Fn wfn 3177  -->wf 3178

This theorem is referenced by:  elmapg 4333  f1domg 4396  fodomfiOLD 4566  fodom 4798  addex 5317  mulex 5318  ser1ft 6328  ser1cl1 6330  ser1recl 6331  ser1ref 6332  ser1mono 6337  ser1add2 6338  ser1add 6339  serzcl1 6562  ser0cl1 6564  ser0f 6565  ser1absdiflem 6929  serzref 7051  serzmulc 7058  ser0mulc 7059  ser1mulc 7060  climfnn 7092  caucvg3a 7164  caucvg3lem 7166  ser1f0 7170  ser1cmp 7174  ser1cmp2 7177  isumsplit 7216  isum0split 7217  elcncf 7265  ruclem5 7514  ismeti 7802  metcn4i 7972  isgrpi 8042  isgrp2i 8076  vcoprne 8198  isvc 8200  isnv 8231  cnnvnm 8312  abscn 8343  islno 8414  hvmulex 8881  hhph 9045  hcau 9051  hlim2 9060  chlim 9104  hhssnm 9131  hhsssh2 9140  elcnopt 9783  ellnopt 9784  elunopt 9799  elhmopt 9800  elcnfnt 9809  ellnfnt 9810  adjvalt 9814  adjeqt 9859  leoprf2t 10060  stelt 10141  hstelt 10142  elghomlem2 10383  elsymgrn 10401  mapdiscn 10511

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693  ax-sep 2703  ax-pow 2742  ax-pr 2779  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-rex 1650  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-id 2835  df-xp 3184  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fun 3192  df-fn 3193  df-f 3194

Copyright terms: Public domain