MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnfvrnss Structured version   Visualization version   GIF version

Theorem fnfvrnss 7123
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
StepHypRef Expression
1 ffnfv 7121 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
2 frn 6725 . 2 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
31, 2sylbir 234 1 ((𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵) → ran 𝐹𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2105  wral 3060  wss 3949  ran crn 5678   Fn wfn 6539  wf 6540  cfv 6544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552
This theorem is referenced by:  ffvresb  7127  dffi3  9429  infxpenlem  10011  alephsing  10274  seqexw  13987  srgfcl  20091  mplind  21851  1stckgenlem  23278  psmetxrge0  24040  plyreres  26029  aannenlem1  26074  subuhgr  28807  subupgr  28808  subumgr  28809  subusgr  28810  elrspunidl  32817  rmulccn  33203  esumfsup  33363  sxbrsigalem3  33566  sitgf  33641  gg-rmulccn  35466  ctbssinf  36591  dihf11lem  40441  hdmaprnN  41039  hgmaprnN  41076  ofoafg  42407  naddcnff  42415  ntrrn  43176  mnurndlem1  43343  volicoff  45011  dirkercncflem2  45120  fourierdlem15  45138  fourierdlem42  45165
  Copyright terms: Public domain W3C validator