Theorem applams ≪ | index | src | ≫

theorem applams {x: nat} (a b: nat x): $ (\ x, a) @ b = N[b / x] a $;

Step	Hyp	Ref	Expression
1		lamisf	isfun (\ x, a)
2	1	a1i	T. -> isfun (\ x, a)
3		nfv	F/ z p = x, a
4		nfnv	FN/ x z
5		nfsbn1	FN/ x N[z / x] a
6	4, 5	nfpr	FN/ x z, N[z / x] a
7	6	nfeq2	F/ x p = z, N[z / x] a
8		id	x = z -> x = z
9		sbnq	x = z -> a = N[z / x] a
10	8, 9	preqd	x = z -> x, a = z, N[z / x] a
11	10	eqeq2d	x = z -> (p = x, a <-> p = z, N[z / x] a)
12	3, 7, 11	cbvexh	E. x p = x, a <-> E. z p = z, N[z / x] a
13		eqeq1	p = b, N[b / x] a -> (p = z, N[z / x] a <-> b, N[b / x] a = z, N[z / x] a)
14	13	exeqd	p = b, N[b / x] a -> (E. z p = z, N[z / x] a <-> E. z b, N[b / x] a = z, N[z / x] a)
15	12, 14	syl5bb	p = b, N[b / x] a -> (E. x p = x, a <-> E. z b, N[b / x] a = z, N[z / x] a)
16	15	elabe	b, N[b / x] a e. {p \| E. x p = x, a} <-> E. z b, N[b / x] a = z, N[z / x] a
17	16	conv lam	b, N[b / x] a e. \ x, a <-> E. z b, N[b / x] a = z, N[z / x] a
18		id	z = b -> z = b
19		sbneq1	z = b -> N[z / x] a = N[b / x] a
20	18, 19	preqd	z = b -> z, N[z / x] a = b, N[b / x] a
21	20	eqeq2d	z = b -> (b, N[b / x] a = z, N[z / x] a <-> b, N[b / x] a = b, N[b / x] a)
22	21	iexe	b, N[b / x] a = b, N[b / x] a -> E. z b, N[b / x] a = z, N[z / x] a
23		eqid	b, N[b / x] a = b, N[b / x] a
24	22, 23	ax_mp	E. z b, N[b / x] a = z, N[z / x] a
25	17, 24	mpbir	b, N[b / x] a e. \ x, a
26	25	a1i	T. -> b, N[b / x] a e. \ x, a
27	2, 26	isfappd	T. -> (\ x, a) @ b = N[b / x] a
28	27	trud	(\ x, a) @ b = N[b / x] 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)