theorem funceq0 (A B F: set): $ func F A B -> (F == 0 <-> A == 0) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmeq0 | Dom F == 0 <-> F == 0 |
|
2 | funcdm | func F A B -> Dom F == A |
|
3 | 2 | eqseq1d | func F A B -> (Dom F == 0 <-> A == 0) |
4 | 1, 3 | syl5bbr | func F A B -> (F == 0 <-> A == 0) |