Theorem lameqb ≪ | index | src | ≫ 

theorem lameqb {x: nat} (a b: nat x): $ A. x a = b <-> \ x, a == \ x, b $;
StepHypRefExpression
1 lameq 
A. x a = b -> \ x, a == \ x, b
2 abeqb 
A. p (E. x p = x, a <-> E. x p = x, b) <-> {p | E. x p = x, a} == {p | E. x p = x, b}
3 2 conv lam 
A. p (E. x p = x, a <-> E. x p = x, b) <-> \ x, a == \ x, b
4 nfv 
F/ y a = b
5 nfsbn1 
FN/ x N[y / x] a
6 nfsbn1 
FN/ x N[y / x] b
7 5, 6 nf_eq 
F/ x N[y / x] a = N[y / x] b
8 sbnq 
x = y -> a = N[y / x] a
9 sbnq 
x = y -> b = N[y / x] b
10 8, 9 eqeqd 
x = y -> (a = b <-> N[y / x] a = N[y / x] b)
11 4, 7, 10 cbvalh 
A. x a = b <-> A. y N[y / x] a = N[y / x] b
12 prth 
y, N[y / x] a = z, N[z / x] b <-> y = z /\ N[y / x] a = N[z / x] b
13 sbneq1 
y = z -> N[y / x] b = N[z / x] b
14 13 eqeq2d 
y = z -> (N[y / x] a = N[y / x] b <-> N[y / x] a = N[z / x] b)
15 14 bi2d 
y = z -> N[y / x] a = N[z / x] b -> N[y / x] a = N[y / x] b
16 15 imp 
y = z /\ N[y / x] a = N[z / x] b -> N[y / x] a = N[y / x] b
17 12, 16 sylbi 
y, N[y / x] a = z, N[z / x] b -> N[y / x] a = N[y / x] b
18 17 eex 
E. z y, N[y / x] a = z, N[z / x] b -> N[y / x] a = N[y / x] b
19 id 
z = y -> z = y
20 sbneq1 
z = y -> N[z / x] a = N[y / x] a
21 19, 20 preqd 
z = y -> z, N[z / x] a = y, N[y / x] a
22 21 eqeq2d 
z = y -> (y, N[y / x] a = z, N[z / x] a <-> y, N[y / x] a = y, N[y / x] a)
23 22 iexe 
y, N[y / x] a = y, N[y / x] a -> E. z y, N[y / x] a = z, N[z / x] a
24 eqid 
y, N[y / x] a = y, N[y / x] a
25 23, 24 ax_mp 
E. z y, N[y / x] a = z, N[z / x] a
26 nfv 
F/ z p = x, a
27 nfnv 
FN/ x z
28 nfsbn1 
FN/ x N[z / x] a
29 27, 28 nfpr 
FN/ x z, N[z / x] a
30 29 nfeq2 
F/ x p = z, N[z / x] a
31 id 
x = z -> x = z
32 sbnq 
x = z -> a = N[z / x] a
33 31, 32 preqd 
x = z -> x, a = z, N[z / x] a
34 33 eqeq2d 
x = z -> (p = x, a <-> p = z, N[z / x] a)
35 26, 30, 34 cbvexh 
E. x p = x, a <-> E. z p = z, N[z / x] a
36 eqeq1 
p = y, N[y / x] a -> (p = z, N[z / x] a <-> y, N[y / x] a = z, N[z / x] a)
37 36 exeqd 
p = y, N[y / x] a -> (E. z p = z, N[z / x] a <-> E. z y, N[y / x] a = z, N[z / x] a)
38 35, 37 syl5bb 
p = y, N[y / x] a -> (E. x p = x, a <-> E. z y, N[y / x] a = z, N[z / x] a)
39 nfv 
F/ z p = x, b
40 nfsbn1 
FN/ x N[z / x] b
41 27, 40 nfpr 
FN/ x z, N[z / x] b
42 41 nfeq2 
F/ x p = z, N[z / x] b
43 sbnq 
x = z -> b = N[z / x] b
44 31, 43 preqd 
x = z -> x, b = z, N[z / x] b
45 44 eqeq2d 
x = z -> (p = x, b <-> p = z, N[z / x] b)
46 39, 42, 45 cbvexh 
E. x p = x, b <-> E. z p = z, N[z / x] b
47 eqeq1 
p = y, N[y / x] a -> (p = z, N[z / x] b <-> y, N[y / x] a = z, N[z / x] b)
48 47 exeqd 
p = y, N[y / x] a -> (E. z p = z, N[z / x] b <-> E. z y, N[y / x] a = z, N[z / x] b)
49 46, 48 syl5bb 
p = y, N[y / x] a -> (E. x p = x, b <-> E. z y, N[y / x] a = z, N[z / x] b)
50 38, 49 bieqd 
p = y, N[y / x] a -> (E. x p = x, a <-> E. x p = x, b <-> (E. z y, N[y / x] a = z, N[z / x] a <-> E. z y, N[y / x] a = z, N[z / x] b))
51 50 eale 
A. p (E. x p = x, a <-> E. x p = x, b) -> (E. z y, N[y / x] a = z, N[z / x] a <-> E. z y, N[y / x] a = z, N[z / x] b)
52 25, 51 mpbii 
A. p (E. x p = x, a <-> E. x p = x, b) -> E. z y, N[y / x] a = z, N[z / x] b
53 18, 52 syl 
A. p (E. x p = x, a <-> E. x p = x, b) -> N[y / x] a = N[y / x] b
54 53 iald 
A. p (E. x p = x, a <-> E. x p = x, b) -> A. y N[y / x] a = N[y / x] b
55 11, 54 sylibr 
A. p (E. x p = x, a <-> E. x p = x, b) -> A. x a = b
56 3, 55 sylbir 
\ x, a == \ x, b -> A. x a = b
57 1, 56 ibii 
A. x a = b <-> \ x, a == \ x, 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)