Step | Hyp | Ref | Expression |
1 |
|
bitr4 |
(a1 e. Arrow a (sn b) <-> func a1 a (sn b)) -> (a1 e. sn (\. x e. a, b) <-> func a1 a (sn b)) -> (a1 e. Arrow a (sn b) <-> a1 e. sn (\. x e. a, b)) |
2 |
|
elArrow |
a1 e. Arrow a (sn b) <-> func a1 a (sn b) |
3 |
1, 2 |
ax_mp |
(a1 e. sn (\. x e. a, b) <-> func a1 a (sn b)) -> (a1 e. Arrow a (sn b) <-> a1 e. sn (\. x e. a, b)) |
4 |
|
bitr4 |
(a1 e. sn (\. x e. a, b) <-> a1 = \. x e. a, b) -> (func a1 a (sn b) <-> a1 = \. x e. a, b) -> (a1 e. sn (\. x e. a, b) <-> func a1 a (sn b)) |
5 |
|
elsn |
a1 e. sn (\. x e. a, b) <-> a1 = \. x e. a, b |
6 |
4, 5 |
ax_mp |
(func a1 a (sn b) <-> a1 = \. x e. a, b) -> (a1 e. sn (\. x e. a, b) <-> func a1 a (sn b)) |
7 |
|
bitr |
(func a1 a (sn b) <-> a1 == \. x e. a, b) -> (a1 == \. x e. a, b <-> a1 = \. x e. a, b) -> (func a1 a (sn b) <-> a1 = \. x e. a, b) |
8 |
|
funcsn2 |
func a1 a (sn b) <-> a1 == \. x e. a, b |
9 |
7, 8 |
ax_mp |
(a1 == \. x e. a, b <-> a1 = \. x e. a, b) -> (func a1 a (sn b) <-> a1 = \. x e. a, b) |
10 |
|
nsinj |
a1 == \. x e. a, b <-> a1 = \. x e. a, b |
11 |
9, 10 |
ax_mp |
func a1 a (sn b) <-> a1 = \. x e. a, b |
12 |
6, 11 |
ax_mp |
a1 e. sn (\. x e. a, b) <-> func a1 a (sn b) |
13 |
3, 12 |
ax_mp |
a1 e. Arrow a (sn b) <-> a1 e. sn (\. x e. a, b) |
14 |
13 |
ax_gen |
A. a1 (a1 e. Arrow a (sn b) <-> a1 e. sn (\. x e. a, b)) |
15 |
14 |
conv eqs |
Arrow a (sn b) == sn (\. x e. a, b) |