Theorem allnth ≪ | index | src | ≫ 

theorem allnth (A: set) (l: nat) {n x: nat}:
  $ all A l <-> A. n A. x (nth n l = suc x -> x e. A) $;
StepHypRefExpression
1 bitr4 
(all A l <-> A. x (E. n nth n l = suc x -> x e. A)) ->
  (A. n A. x (nth n l = suc x -> x e. A) <-> A. x (E. n nth n l = suc x -> x e. A)) ->
  (all A l <-> A. n A. x (nth n l = suc x -> x e. A))
2 lmemnth 
x IN l <-> E. n nth n l = suc x
3 2 conv lmem 
x e. lmems l <-> E. n nth n l = suc x
4 3 imeq1i 
x e. lmems l -> x e. A <-> E. n nth n l = suc x -> x e. A
5 4 aleqi 
A. x (x e. lmems l -> x e. A) <-> A. x (E. n nth n l = suc x -> x e. A)
6 5 conv all, subset 
all A l <-> A. x (E. n nth n l = suc x -> x e. A)
7 1, 6 ax_mp 
(A. n A. x (nth n l = suc x -> x e. A) <-> A. x (E. n nth n l = suc x -> x e. A)) -> (all A l <-> A. n A. x (nth n l = suc x -> x e. A))
8 bitr4 
(A. n A. x (nth n l = suc x -> x e. A) <-> A. x A. n (nth n l = suc x -> x e. A)) ->
  (A. x (E. n nth n l = suc x -> x e. A) <-> A. x A. n (nth n l = suc x -> x e. A)) ->
  (A. n A. x (nth n l = suc x -> x e. A) <-> A. x (E. n nth n l = suc x -> x e. A))
9 alcomb 
A. n A. x (nth n l = suc x -> x e. A) <-> A. x A. n (nth n l = suc x -> x e. A)
10 8, 9 ax_mp 
(A. x (E. n nth n l = suc x -> x e. A) <-> A. x A. n (nth n l = suc x -> x e. A)) ->
  (A. n A. x (nth n l = suc x -> x e. A) <-> A. x (E. n nth n l = suc x -> x e. A))
11 eexb 
E. n nth n l = suc x -> x e. A <-> A. n (nth n l = suc x -> x e. A)
12 11 aleqi 
A. x (E. n nth n l = suc x -> x e. A) <-> A. x A. n (nth n l = suc x -> x e. A)
13 10, 12 ax_mp 
A. n A. x (nth n l = suc x -> x e. A) <-> A. x (E. n nth n l = suc x -> x e. A)
14 7, 13 ax_mp 
all A l <-> A. n A. x (nth n l = suc x -> x e. A)

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)