Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > f0 | Structured version Visualization version GIF version |
Description: The empty function. (Contributed by NM, 14-Aug-1999.) |
Ref | Expression |
---|---|
f0 | ⊢ ∅:∅⟶𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2821 | . . 3 ⊢ ∅ = ∅ | |
2 | fn0 6473 | . . 3 ⊢ (∅ Fn ∅ ↔ ∅ = ∅) | |
3 | 1, 2 | mpbir 232 | . 2 ⊢ ∅ Fn ∅ |
4 | rn0 5790 | . . 3 ⊢ ran ∅ = ∅ | |
5 | 0ss 4349 | . . 3 ⊢ ∅ ⊆ 𝐴 | |
6 | 4, 5 | eqsstri 4000 | . 2 ⊢ ran ∅ ⊆ 𝐴 |
7 | df-f 6353 | . 2 ⊢ (∅:∅⟶𝐴 ↔ (∅ Fn ∅ ∧ ran ∅ ⊆ 𝐴)) | |
8 | 3, 6, 7 | mpbir2an 707 | 1 ⊢ ∅:∅⟶𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ⊆ wss 3935 ∅c0 4290 ran crn 5550 Fn wfn 6344 ⟶wf 6345 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-br 5059 df-opab 5121 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-fun 6351 df-fn 6352 df-f 6353 |
This theorem is referenced by: f00 6555 f0bi 6556 f10 6641 map0g 8438 ac6sfi 8751 oif 8983 wrd0 13879 0csh0 14145 ram0 16348 0ssc 17097 0subcat 17098 gsum0 17884 ga0 18368 0frgp 18836 ptcmpfi 22351 0met 22905 perfdvf 24430 uhgr0e 26784 uhgr0 26786 griedg0prc 26974 locfinref 31005 matunitlindf 34772 poimirlem28 34802 climlimsupcex 41930 0cnf 42040 dvnprodlem3 42113 sge00 42539 hoidmvlelem3 42760 |
Copyright terms: Public domain | W3C validator |