Theorem f0 6653

Description: The empty function. (Contributed by NM, 14-Aug-1999.)

Assertion

Ref	Expression
f0	⊢ ∅:∅⟶𝐴

Proof of Theorem f0

Step	Hyp	Ref	Expression
1		eqid 2740	. . 3 ⊢ ∅ = ∅
2		fn0 6562	. . 3 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
3	1, 2	mpbir 230	. 2 ⊢ ∅ Fn ∅
4		rn0 5834	. . 3 ⊢ ran ∅ = ∅
5		0ss 4336	. . 3 ⊢ ∅ ⊆ 𝐴
6	4, 5	eqsstri 3960	. 2 ⊢ ran ∅ ⊆ 𝐴
7		df-f 6436	. 2 ⊢ (∅:∅⟶𝐴 ↔ (∅ Fn ∅ ∧ ran ∅ ⊆ 𝐴))
8	3, 6, 7	mpbir2an 708	1 ⊢ ∅:∅⟶𝐴

Syntax hints:   = wceq 1542   ⊆ wss 3892  ∅c0 4262  ran crn 5591   Fn wfn 6427  ⟶wf 6428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080  df-opab 5142  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-fun 6434  df-fn 6435  df-f 6436

This theorem is referenced by:  f00  6654  f0bi  6655  f10  6746  map0g  8655  ac6sfi  9036  oif  9267  wrd0  14240  0csh0  14504  ram0  16721  0ssc  17550  0subcat  17551  setc2ohom  17808  cat1lem  17809  gsum0  18366  ga0  18902  0frgp  19383  ptcmpfi  22962  0met  23517  perfdvf  25065  uhgr0e  27439  uhgr0  27441  griedg0prc  27629  locfinref  31787  matunitlindf  35771  poimirlem28  35801  sticksstones11  40109  climlimsupcex  43281  0cnf  43389  dvnprodlem3  43460  sge00  43885  hoidmvlelem3  44106