Theorem f0 6562

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

Assertion

Ref	Expression
f0	⊢ ∅:∅⟶𝐴

Proof of Theorem f0

Step	Hyp	Ref	Expression
1		eqid 2823	. . 3 ⊢ ∅ = ∅
2		fn0 6481	. . 3 ⊢ (∅ Fn ∅ ↔ ∅ = ∅)
3	1, 2	mpbir 233	. 2 ⊢ ∅ Fn ∅
4		rn0 5798	. . 3 ⊢ ran ∅ = ∅
5		0ss 4352	. . 3 ⊢ ∅ ⊆ 𝐴
6	4, 5	eqsstri 4003	. 2 ⊢ ran ∅ ⊆ 𝐴
7		df-f 6361	. 2 ⊢ (∅:∅⟶𝐴 ↔ (∅ Fn ∅ ∧ ran ∅ ⊆ 𝐴))
8	3, 6, 7	mpbir2an 709	1 ⊢ ∅:∅⟶𝐴

Syntax hints:   = wceq 1537   ⊆ wss 3938  ∅c0 4293  ran crn 5558   Fn wfn 6352  ⟶wf 6353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-fun 6359  df-fn 6360  df-f 6361

This theorem is referenced by:  f00  6563  f0bi  6564  f10  6649  map0g  8450  ac6sfi  8764  oif  8996  wrd0  13891  0csh0  14157  ram0  16360  0ssc  17109  0subcat  17110  gsum0  17896  ga0  18430  0frgp  18907  ptcmpfi  22423  0met  22978  perfdvf  24503  uhgr0e  26858  uhgr0  26860  griedg0prc  27048  locfinref  31107  matunitlindf  34892  poimirlem28  34922  climlimsupcex  42057  0cnf  42167  dvnprodlem3  42240  sge00  42665  hoidmvlelem3  42886