Step |
Hyp |
Ref |
Expression |
1 |
|
df-id |
|- _I = { <. x , z >. | x = z } |
2 |
|
equcom |
|- ( x = z <-> z = x ) |
3 |
2
|
anbi1ci |
|- ( ( w = <. x , z >. /\ x = z ) <-> ( z = x /\ w = <. x , z >. ) ) |
4 |
3
|
exbii |
|- ( E. z ( w = <. x , z >. /\ x = z ) <-> E. z ( z = x /\ w = <. x , z >. ) ) |
5 |
|
opeq2 |
|- ( z = x -> <. x , z >. = <. x , x >. ) |
6 |
5
|
eqeq2d |
|- ( z = x -> ( w = <. x , z >. <-> w = <. x , x >. ) ) |
7 |
6
|
equsexvw |
|- ( E. z ( z = x /\ w = <. x , z >. ) <-> w = <. x , x >. ) |
8 |
|
equid |
|- x = x |
9 |
8
|
biantru |
|- ( w = <. x , x >. <-> ( w = <. x , x >. /\ x = x ) ) |
10 |
4 7 9
|
3bitri |
|- ( E. z ( w = <. x , z >. /\ x = z ) <-> ( w = <. x , x >. /\ x = x ) ) |
11 |
10
|
exbii |
|- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x ( w = <. x , x >. /\ x = x ) ) |
12 |
|
nfe1 |
|- F/ x E. x ( w = <. x , x >. /\ x = x ) |
13 |
12
|
19.9 |
|- ( E. x E. x ( w = <. x , x >. /\ x = x ) <-> E. x ( w = <. x , x >. /\ x = x ) ) |
14 |
11 13
|
bitr4i |
|- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x E. x ( w = <. x , x >. /\ x = x ) ) |
15 |
|
opeq2 |
|- ( x = y -> <. x , x >. = <. x , y >. ) |
16 |
15
|
eqeq2d |
|- ( x = y -> ( w = <. x , x >. <-> w = <. x , y >. ) ) |
17 |
|
equequ2 |
|- ( x = y -> ( x = x <-> x = y ) ) |
18 |
16 17
|
anbi12d |
|- ( x = y -> ( ( w = <. x , x >. /\ x = x ) <-> ( w = <. x , y >. /\ x = y ) ) ) |
19 |
18
|
sps |
|- ( A. x x = y -> ( ( w = <. x , x >. /\ x = x ) <-> ( w = <. x , y >. /\ x = y ) ) ) |
20 |
19
|
drex1 |
|- ( A. x x = y -> ( E. x ( w = <. x , x >. /\ x = x ) <-> E. y ( w = <. x , y >. /\ x = y ) ) ) |
21 |
20
|
drex2 |
|- ( A. x x = y -> ( E. x E. x ( w = <. x , x >. /\ x = x ) <-> E. x E. y ( w = <. x , y >. /\ x = y ) ) ) |
22 |
14 21
|
syl5bb |
|- ( A. x x = y -> ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x E. y ( w = <. x , y >. /\ x = y ) ) ) |
23 |
|
nfnae |
|- F/ x -. A. x x = y |
24 |
|
nfnae |
|- F/ y -. A. x x = y |
25 |
|
nfcvd |
|- ( -. A. x x = y -> F/_ y w ) |
26 |
|
nfcvf2 |
|- ( -. A. x x = y -> F/_ y x ) |
27 |
|
nfcvd |
|- ( -. A. x x = y -> F/_ y z ) |
28 |
26 27
|
nfopd |
|- ( -. A. x x = y -> F/_ y <. x , z >. ) |
29 |
25 28
|
nfeqd |
|- ( -. A. x x = y -> F/ y w = <. x , z >. ) |
30 |
26 27
|
nfeqd |
|- ( -. A. x x = y -> F/ y x = z ) |
31 |
29 30
|
nfand |
|- ( -. A. x x = y -> F/ y ( w = <. x , z >. /\ x = z ) ) |
32 |
|
opeq2 |
|- ( z = y -> <. x , z >. = <. x , y >. ) |
33 |
32
|
eqeq2d |
|- ( z = y -> ( w = <. x , z >. <-> w = <. x , y >. ) ) |
34 |
|
equequ2 |
|- ( z = y -> ( x = z <-> x = y ) ) |
35 |
33 34
|
anbi12d |
|- ( z = y -> ( ( w = <. x , z >. /\ x = z ) <-> ( w = <. x , y >. /\ x = y ) ) ) |
36 |
35
|
a1i |
|- ( -. A. x x = y -> ( z = y -> ( ( w = <. x , z >. /\ x = z ) <-> ( w = <. x , y >. /\ x = y ) ) ) ) |
37 |
24 31 36
|
cbvexd |
|- ( -. A. x x = y -> ( E. z ( w = <. x , z >. /\ x = z ) <-> E. y ( w = <. x , y >. /\ x = y ) ) ) |
38 |
23 37
|
exbid |
|- ( -. A. x x = y -> ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x E. y ( w = <. x , y >. /\ x = y ) ) ) |
39 |
22 38
|
pm2.61i |
|- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x E. y ( w = <. x , y >. /\ x = y ) ) |
40 |
39
|
abbii |
|- { w | E. x E. z ( w = <. x , z >. /\ x = z ) } = { w | E. x E. y ( w = <. x , y >. /\ x = y ) } |
41 |
|
df-opab |
|- { <. x , z >. | x = z } = { w | E. x E. z ( w = <. x , z >. /\ x = z ) } |
42 |
|
df-opab |
|- { <. x , y >. | x = y } = { w | E. x E. y ( w = <. x , y >. /\ x = y ) } |
43 |
40 41 42
|
3eqtr4i |
|- { <. x , z >. | x = z } = { <. x , y >. | x = y } |
44 |
1 43
|
eqtri |
|- _I = { <. x , y >. | x = y } |