Theorem f0 6723

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

Assertion

Ref	Expression
f0	⊢ ∅:∅⟶𝐴

Proof of Theorem f0

Step	Hyp	Ref	Expression
1		eqid 2737	. . 3 ⊢ ∅ = ∅
2		fn0 6631	. . 3 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
3	1, 2	mpbir 231	. 2 ⊢ ∅ Fn ∅
4		rn0 5883	. . 3 ⊢ ran ∅ = ∅
5		0ss 4354	. . 3 ⊢ ∅ ⊆ 𝐴
6	4, 5	eqsstri 3982	. 2 ⊢ ran ∅ ⊆ 𝐴
7		df-f 6504	. 2 ⊢ (∅:∅⟶𝐴 ↔ (∅ Fn ∅ ∧ ran ∅ ⊆ 𝐴))
8	3, 6, 7	mpbir2an 712	1 ⊢ ∅:∅⟶𝐴

Syntax hints:   = wceq 1542   ⊆ wss 3903  ∅c0 4287  ran crn 5633   Fn wfn 6495  ⟶wf 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  f00  6724  f0bi  6725  f10  6815  map0g  8834  ac6sfi  9196  oif  9447  wrd0  14474  0csh0  14728  ram0  16962  0ssc  17773  0subcat  17774  setc2ohom  18031  cat1lem  18032  gsum0  18621  ga0  19239  0frgp  19720  ptcmpfi  23769  0met  24322  perfdvf  25872  uhgr0e  29156  uhgr0  29158  griedg0prc  29349  locfinref  34018  matunitlindf  37863  poimirlem28  37893  sticksstones11  42520  climlimsupcex  46121  0cnf  46229  dvnprodlem3  46300  sge00  46728  hoidmvlelem3  46949