Step |
Hyp |
Ref |
Expression |
1 |
|
idn1 |
|- (. A e. B ->. A e. B ). |
2 |
|
eqsbc3 |
|- ( A e. B -> ( [. A / x ]. x = C <-> A = C ) ) |
3 |
1 2
|
e1a |
|- (. A e. B ->. ( [. A / x ]. x = C <-> A = C ) ). |
4 |
|
eqcom |
|- ( C = x <-> x = C ) |
5 |
4
|
sbcbii |
|- ( [. A / x ]. C = x <-> [. A / x ]. x = C ) |
6 |
5
|
a1i |
|- ( A e. B -> ( [. A / x ]. C = x <-> [. A / x ]. x = C ) ) |
7 |
1 6
|
e1a |
|- (. A e. B ->. ( [. A / x ]. C = x <-> [. A / x ]. x = C ) ). |
8 |
|
idn2 |
|- (. A e. B ,. [. A / x ]. C = x ->. [. A / x ]. C = x ). |
9 |
|
biimp |
|- ( ( [. A / x ]. C = x <-> [. A / x ]. x = C ) -> ( [. A / x ]. C = x -> [. A / x ]. x = C ) ) |
10 |
7 8 9
|
e12 |
|- (. A e. B ,. [. A / x ]. C = x ->. [. A / x ]. x = C ). |
11 |
|
biimp |
|- ( ( [. A / x ]. x = C <-> A = C ) -> ( [. A / x ]. x = C -> A = C ) ) |
12 |
3 10 11
|
e12 |
|- (. A e. B ,. [. A / x ]. C = x ->. A = C ). |
13 |
|
eqcom |
|- ( A = C <-> C = A ) |
14 |
12 13
|
e2bi |
|- (. A e. B ,. [. A / x ]. C = x ->. C = A ). |
15 |
14
|
in2 |
|- (. A e. B ->. ( [. A / x ]. C = x -> C = A ) ). |
16 |
|
idn2 |
|- (. A e. B ,. C = A ->. C = A ). |
17 |
16 13
|
e2bir |
|- (. A e. B ,. C = A ->. A = C ). |
18 |
|
biimpr |
|- ( ( [. A / x ]. x = C <-> A = C ) -> ( A = C -> [. A / x ]. x = C ) ) |
19 |
3 17 18
|
e12 |
|- (. A e. B ,. C = A ->. [. A / x ]. x = C ). |
20 |
|
biimpr |
|- ( ( [. A / x ]. C = x <-> [. A / x ]. x = C ) -> ( [. A / x ]. x = C -> [. A / x ]. C = x ) ) |
21 |
7 19 20
|
e12 |
|- (. A e. B ,. C = A ->. [. A / x ]. C = x ). |
22 |
21
|
in2 |
|- (. A e. B ->. ( C = A -> [. A / x ]. C = x ) ). |
23 |
|
impbi |
|- ( ( [. A / x ]. C = x -> C = A ) -> ( ( C = A -> [. A / x ]. C = x ) -> ( [. A / x ]. C = x <-> C = A ) ) ) |
24 |
15 22 23
|
e11 |
|- (. A e. B ->. ( [. A / x ]. C = x <-> C = A ) ). |
25 |
24
|
in1 |
|- ( A e. B -> ( [. A / x ]. C = x <-> C = A ) ) |