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

Theorem f0 5748
Description: The empty function. (Contributed by NM, 14-Aug-1999.)
Assertion
Ref Expression
f0  |-  (/) : (/) --> A

Proof of Theorem f0
StepHypRef Expression
1 eqid 2454 . . 3  |-  (/)  =  (/)
2 fn0 5682 . . 3  |-  ( (/)  Fn  (/) 
<->  (/)  =  (/) )
31, 2mpbir 209 . 2  |-  (/)  Fn  (/)
4 rn0 5243 . . 3  |-  ran  (/)  =  (/)
5 0ss 3813 . . 3  |-  (/)  C_  A
64, 5eqsstri 3519 . 2  |-  ran  (/)  C_  A
7 df-f 5574 . 2  |-  ( (/) :
(/) --> A  <->  ( (/)  Fn  (/)  /\  ran  (/)  C_  A ) )
83, 6, 7mpbir2an 918 1  |-  (/) : (/) --> A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398    C_ wss 3461   (/)c0 3783   ran crn 4989    Fn wfn 5565   -->wf 5566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-fun 5572  df-fn 5573  df-f 5574
This theorem is referenced by:  f00  5749  f0bi  5750  f10  5829  fconstfvOLD  6109  map0g  7451  ac6sfi  7756  oif  7947  wrd0  12553  wrd0OLD  12554  0csh0  12755  ram0  14624  0ssc  15325  0subcat  15326  gsum0  16104  ga0  16535  0frgp  16996  ptcmpfi  20480  0met  21035  perfdvf  22473  uhgra0  24511  umgra0  24527  vdgr0  25102  locfinref  28079  0cnf  31918  dvnprodlem3  31984  mbf0  31995  uhg0e  32748
  Copyright terms: Public domain W3C validator