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

Theorem f0 6724
Description: The empty function. (Contributed by NM, 14-Aug-1999.)
Assertion
Ref Expression
f0 ∅:∅⟶𝐴

Proof of Theorem f0
StepHypRef Expression
1 eqid 2737 . . 3 ∅ = ∅
2 fn0 6633 . . 3 (∅ Fn ∅ ↔ ∅ = ∅)
31, 2mpbir 230 . 2 ∅ Fn ∅
4 rn0 5882 . . 3 ran ∅ = ∅
5 0ss 4357 . . 3 ∅ ⊆ 𝐴
64, 5eqsstri 3979 . 2 ran ∅ ⊆ 𝐴
7 df-f 6501 . 2 (∅:∅⟶𝐴 ↔ (∅ Fn ∅ ∧ ran ∅ ⊆ 𝐴))
83, 6, 7mpbir2an 710 1 ∅:∅⟶𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wss 3911  c0 4283  ran crn 5635   Fn wfn 6492  wf 6493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-fun 6499  df-fn 6500  df-f 6501
This theorem is referenced by:  f00  6725  f0bi  6726  f10  6818  map0g  8823  ac6sfi  9232  oif  9467  wrd0  14428  0csh0  14682  ram0  16895  0ssc  17724  0subcat  17725  setc2ohom  17982  cat1lem  17983  gsum0  18540  ga0  19079  0frgp  19562  ptcmpfi  23167  0met  23722  perfdvf  25270  uhgr0e  28025  uhgr0  28027  griedg0prc  28215  locfinref  32425  matunitlindf  36079  poimirlem28  36109  sticksstones11  40567  climlimsupcex  44017  0cnf  44125  dvnprodlem3  44196  sge00  44624  hoidmvlelem3  44845
  Copyright terms: Public domain W3C validator