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) $;

Step	Hyp	Ref	Expression
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	6	bitr4*	(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	9	bitr4*	(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	9, 12	bitr4*	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	6, 13	bitr4*	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)