Theorem Arrow01 | index | src |

theorem Arrow01 (B: set): $ Arrow 0 B == sn 0 $;
StepHypRefExpression
1 bitr4
(a1 e. Arrow 0 B <-> func a1 0 B) -> (a1 e. sn 0 <-> func a1 0 B) -> (a1 e. Arrow 0 B <-> a1 e. sn 0)
2 elArrow
a1 e. Arrow 0 B <-> func a1 0 B
3 1, 2 ax_mp
(a1 e. sn 0 <-> func a1 0 B) -> (a1 e. Arrow 0 B <-> a1 e. sn 0)
4 bitr4
(a1 e. sn 0 <-> a1 = 0) -> (func a1 0 B <-> a1 = 0) -> (a1 e. sn 0 <-> func a1 0 B)
5 elsn
a1 e. sn 0 <-> a1 = 0
6 4, 5 ax_mp
(func a1 0 B <-> a1 = 0) -> (a1 e. sn 0 <-> func a1 0 B)
7 bitr
(func a1 0 B <-> a1 == 0) -> (a1 == 0 <-> a1 = 0) -> (func a1 0 B <-> a1 = 0)
8 func02
func a1 0 B <-> a1 == 0
9 7, 8 ax_mp
(a1 == 0 <-> a1 = 0) -> (func a1 0 B <-> a1 = 0)
10 nsinj
a1 == 0 <-> a1 = 0
11 9, 10 ax_mp
func a1 0 B <-> a1 = 0
12 6, 11 ax_mp
a1 e. sn 0 <-> func a1 0 B
13 3, 12 ax_mp
a1 e. Arrow 0 B <-> a1 e. sn 0
14 13 ax_gen
A. a1 (a1 e. Arrow 0 B <-> a1 e. sn 0)
15 14 conv eqs
Arrow 0 B == sn 0

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)