Theorem fnfvrnss 7114

Description: An upper bound for range determined by function values. (Contributed by NM, 8-Oct-2004.)

Assertion

Ref	Expression
fnfvrnss	⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹

Proof of Theorem fnfvrnss

Step	Hyp	Ref	Expression
1		ffnfv 7112	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
2		frn 6710	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
3	1, 2	sylbir 238	1 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3076   ⊆ wss 3899  ran crn 5656   Fn wfn 6528  ⟶wf 6529  ‘cfv 6533

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541

This theorem is used by:  ffvresb  7119  dffi3  9401  infxpenlem  10016  alephsing  10278  seqexw  14081  sgnrn  15171  mgmn0plusgf  18741  srgfcl  20335  mplind  22286  1stckgenlem  23779  psmetxrge0  24539  plyreres  26513  aannenlem1  26564  bdayn0sf1o  28635  dfnns2  28637  subuhgr  29746  subupgr  29747  subumgr  29748  subusgr  29749  elrspunidl  33856  rmulccn  34438  esumfsup  34580  sxbrsigalem3  34783  sitgf  34858  ctbssinf  38160  dihf11lem  42139  hdmaprnN  42737  hgmaprnN  42774  ofoafg  44195  naddcnff  44203  ntrrn  44962  mnurndlem1  45105  volicoff  46823  dirkercncflem2  46932  fourierdlem15  46950  fourierdlem42  46977  tmachlem-extpcover  47773  grimuhgr  48803  slotresfo  49825