Theorem prelslams ≪ | index | src | ≫

theorem prelslams (a b: nat) {x: nat} (y: nat) (A: set x):
  $ (a, b), y e. (\\ x, A) <-> b, y e. S[a / x] A $;

Step	Hyp	Ref	Expression
1		sndpr	snd (a, b) = b
2		sndeq	p = a, b -> snd p = snd (a, b)
3	1, 2	syl6eq	p = a, b -> snd p = b
4	3	anwl	p = a, b /\ z = y -> snd p = b
5		anr	p = a, b /\ z = y -> z = y
6	4, 5	preqd	p = a, b /\ z = y -> snd p, z = b, y
7		fstpr	fst (a, b) = a
8		fsteq	p = a, b -> fst p = fst (a, b)
9	7, 8	syl6eq	p = a, b -> fst p = a
10	9	sbseq1d	p = a, b -> S[fst p / x] A == S[a / x] A
11	10	anwl	p = a, b /\ z = y -> S[fst p / x] A == S[a / x] A
12	6, 11	eleqd	p = a, b /\ z = y -> (snd p, z e. S[fst p / x] A <-> b, y e. S[a / x] A)
13	12	elabed	p = a, b -> (y e. {z \| snd p, z e. S[fst p / x] A} <-> b, y e. S[a / x] A)
14	13	elsabe	(a, b), y e. S\ p, {z \| snd p, z e. S[fst p / x] A} <-> b, y e. S[a / x] A
15	14	conv slam	(a, b), y e. (\\ x, A) <-> b, y e. S[a / 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)