Theorem elArray02 ≪ | index | src | ≫ 

theorem elArray02 (A: set) (l: nat): $ l e. Array A 0 <-> l = 0 $;
StepHypRefExpression
1 bitr 
(l e. Array A 0 <-> l e. List A /\ len l = 0) -> (l e. List A /\ len l = 0 <-> l = 0) -> (l e. Array A 0 <-> l = 0)
2 elArray 
l e. Array A 0 <-> l e. List A /\ len l = 0
3 1, 2 ax_mp 
(l e. List A /\ len l = 0 <-> l = 0) -> (l e. Array A 0 <-> l = 0)
4 bitr 
(l e. List A /\ len l = 0 <-> l e. List A /\ l = 0) -> (l e. List A /\ l = 0 <-> l = 0) -> (l e. List A /\ len l = 0 <-> l = 0)
5 leneq0 
len l = 0 <-> l = 0
6 5 aneq2i 
l e. List A /\ len l = 0 <-> l e. List A /\ l = 0
7 4, 6 ax_mp 
(l e. List A /\ l = 0 <-> l = 0) -> (l e. List A /\ len l = 0 <-> l = 0)
8 bian1a 
(l = 0 -> l e. List A) -> (l e. List A /\ l = 0 <-> l = 0)
9 elList0 
0 e. List A
10 eleq1 
l = 0 -> (l e. List A <-> 0 e. List A)
11 9, 10 mpbiri 
l = 0 -> l e. List A
12 8, 11 ax_mp 
l e. List A /\ l = 0 <-> l = 0
13 7, 12 ax_mp 
l e. List A /\ len l = 0 <-> l = 0
14 3, 13 ax_mp 
l e. Array A 0 <-> l = 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)