Theorem sndpr ≪ | index | src | ≫

pub theorem sndpr (a b: nat): $ snd (a, b) = b $;

Step	Hyp	Ref	Expression
1		prth	a, b = x, y <-> a = x /\ b = y
2		anr	a = x /\ b = y -> b = y
3	2	eqcomd	a = x /\ b = y -> y = b
4	1, 3	sylbi	a, b = x, y -> y = b
5	4	eex	E. x a, b = x, y -> y = b
6		preq2	y = b -> a, y = a, b
7	6	eqcomd	y = b -> a, b = a, y
8		preq1	x = a -> x, y = a, y
9	8	eqeq2d	x = a -> (a, b = x, y <-> a, b = a, y)
10	9	iexe	a, b = a, y -> E. x a, b = x, y
11	7, 10	rsyl	y = b -> E. x a, b = x, y
12	5, 11	ibii	E. x a, b = x, y <-> y = b
13	12	a1i	T. -> (E. x a, b = x, y <-> y = b)
14	13	eqtheabd	T. -> the {y \| E. x a, b = x, y} = b
15	14	conv snd	T. -> snd (a, b) = b
16	15	trud	snd (a, b) = b

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)