Theorem fex 7228

Description: If the domain of a mapping is a set, the function is a set. (Contributed by NM, 3-Oct-1999.)

Assertion

Ref	Expression
fex	⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V)

Proof of Theorem fex

Step	Hyp	Ref	Expression
1		ffn 6709	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnex 7219	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V)
3	1, 2	sylan 592	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  Vcvv 3457   Fn wfn 6535  ⟶wf 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548

This theorem is used by:  fexd  7229  f1oexrnex  7926  fsuppeq  8173  suppsnop  8176  f1domg  8970  ffsuppbi  9361  mapfienlem2  9369  oiexg  9500  infxpenc2lem2  10016  isf32lem10  10357  hasheqf1oi  14401  hashf1rn  14402  hashimarn  14491  iswrd  14566  climsup  15741  fsum  15790  supcvg  15929  fprod  16014  vdwmc  17056  vdwpc  17058  elsymgbas  19468  gsumval3a  19997  gsumval3lem1  19999  gsumval3lem2  20000  dmdprd  20094  cnfldfun  21566  cnfldfunALT  21567  tngngp3  24844  climcncf  25090  ulmval  26574  pserulm  26616  isismt  28834  isgrpoi  30897  isvcOLD  30978  isnv  31011  cnnvg  31077  cnnvs  31079  cnnvnm  31080  cncph  31218  ajval  31260  hvmulex  31410  hhph  31577  hlimi  31587  chlimi  31633  hhssva  31656  hhsssm  31657  hhssnm  31658  hhshsslem1  31666  elunop  32271  adjeq  32334  leoprf2  32526  fpwrelmapffslem  33123  ccatws1f1o  33313  lmdvg  34383  esumpfinvallem  34504  omsf  34727  eulerpartgbij  34803  eulerpartlemmf  34806  subfacp1lem5  35689  sinccvglem  36177  poimirlem24  38328  mbfresfi  38350  elghomlem2OLD  38570  islaut  40890  ispautN  40906  istendo  41567  binomcxplemnotnn0  45099  climexp  46354  climinf  46355  stirlinglem8  46828  fourierdlem70  46923  ismea  47198  meadjiunlem  47212  grtriclwlk3  48743  isassintop  49008  fdivmpt  49353  elbigolo1  49370  fucofvalne  50136