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

Theorem dffn3 6558
Description: A function maps to its range. (Contributed by NM, 1-Sep-1999.)
Assertion
Ref Expression
dffn3 (𝐹 Fn 𝐴𝐹:𝐴⟶ran 𝐹)

Proof of Theorem dffn3
StepHypRef Expression
1 ssid 3923 . . 3 ran 𝐹 ⊆ ran 𝐹
21biantru 533 . 2 (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
3 df-f 6384 . 2 (𝐹:𝐴⟶ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ran 𝐹))
42, 3bitr4i 281 1 (𝐹 Fn 𝐴𝐹:𝐴⟶ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  wss 3866  ran crn 5552   Fn wfn 6375  wf 6376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-f 6384
This theorem is referenced by:  ffrn  6559  ffrnb  6560  fsn2  6951  offsplitfpar  7888  fo2ndf  7890  suppcoss  7949  fndmfisuppfi  8997  fndmfifsupp  8998  fin23lem17  9952  fin23lem32  9958  fnct  10151  yoniso  17793  1stckgen  22451  ovolicc2  24419  i1fadd  24592  i1fmul  24593  itg1addlem4  24596  itg1addlem4OLD  24597  i1fmulc  24601  clwlkclwwlklem2  28083  foresf1o  30569  fcoinver  30665  ofpreima2  30723  locfinreflem  31504  pl1cn  31619  fvineqsneu  35319  poimirlem29  35543  poimirlem30  35544  itg2addnclem2  35566  mapdcl  39404  wessf1ornlem  42395  unirnmap  42421  fsneqrn  42424  icccncfext  43103  stoweidlem29  43245  stoweidlem31  43247  stoweidlem59  43275  subsaliuncllem  43571  meadjiunlem  43678  uniimaprimaeqfv  44507  uniimaelsetpreimafv  44521
  Copyright terms: Public domain W3C validator