MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnovrn Unicode version

Theorem fnovrn 6322
Description: An operation's value belongs to its range. (Contributed by NM, 10-Feb-2007.)
Assertion
Ref Expression
fnovrn

Proof of Theorem fnovrn
StepHypRef Expression
1 opelxpi 4953 . . 3
2 df-ov 6177 . . . 4
3 fnfvelrn 5923 . . . 4
42, 3syl5eqel 2540 . . 3
51, 4sylan2 474 . 2
653impb 1184 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 965  e.wcel 1757  <.cop 3965  X.cxp 4920  rancrn 4923  Fnwfn 5495  `cfv 5500  (class class class)co 6174
This theorem is referenced by:  unirnioo  11474  ioorebas  11476  yonffthlem  15178  gsumval2a  15598  efginvrel2  16312  efgredleme  16328  efgcpbllemb  16340  mplsubrglem  17608  mplsubrglemOLD  17609  lecldbas  18923  blelrnps  20091  blelrn  20092  blssioo  20472  tgioo  20473  opnmbllem  21181  mbfdm  21206  mbfima  21210  isgrpo2  23803  tpr2rico  26460  dya2icoseg  26810  opnmbllem0  28549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4495  ax-nul 4503  ax-pr 4613
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3054  df-sbc 3269  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-nul 3720  df-if 3874  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4174  df-br 4375  df-opab 4433  df-id 4718  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-rn 4933  df-iota 5463  df-fun 5502  df-fn 5503  df-fv 5508  df-ov 6177
  Copyright terms: Public domain W3C validator