Step | Hyp | Ref | Expression |
1 |
|
axext2 |
(\\ x, A) @@ a == S[a / x] A <-> A. a1 A. a2 (a1, a2 e. (\\ x, A) @@ a <-> a1, a2 e. S[a / x] A) |
2 |
|
bitr |
(a1, a2 e. (\\ x, A) @@ a <-> (a, a1), a2 e. (\\ x, A)) ->
((a, a1), a2 e. (\\ x, A) <-> a1, a2 e. S[a / x] A) ->
(a1, a2 e. (\\ x, A) @@ a <-> a1, a2 e. S[a / x] A) |
3 |
|
prelsapp |
a1, a2 e. (\\ x, A) @@ a <-> (a, a1), a2 e. (\\ x, A) |
4 |
2, 3 |
ax_mp |
((a, a1), a2 e. (\\ x, A) <-> a1, a2 e. S[a / x] A) -> (a1, a2 e. (\\ x, A) @@ a <-> a1, a2 e. S[a / x] A) |
5 |
|
prelslams |
(a, a1), a2 e. (\\ x, A) <-> a1, a2 e. S[a / x] A |
6 |
4, 5 |
ax_mp |
a1, a2 e. (\\ x, A) @@ a <-> a1, a2 e. S[a / x] A |
7 |
6 |
ax_gen |
A. a2 (a1, a2 e. (\\ x, A) @@ a <-> a1, a2 e. S[a / x] A) |
8 |
7 |
ax_gen |
A. a1 A. a2 (a1, a2 e. (\\ x, A) @@ a <-> a1, a2 e. S[a / x] A) |
9 |
1, 8 |
mpbir |
(\\ x, A) @@ a == S[a / x] A |