Step | Hyp | Ref
| Expression |
1 | | df-rex 2620 |
. . . 4
![(](lp.gif) ![E.](exists.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif)
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif)
![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
2 | | exancom 1586 |
. . . 4
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![A](_ca.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
3 | | vex 2862 |
. . . . . . 7
![_V](rmcv.gif) |
4 | | elp6 4263 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
P6 ∼ 1c k ![_V](rmcv.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![A.](forall.gif) ![z](_z.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ∼ 1c k ![_V](rmcv.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
![(](lp.gif) P6 ∼ 1c k ![_V](rmcv.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![A.](forall.gif) ![z](_z.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ∼ 1c k ![_V](rmcv.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
6 | | elun 3220 |
. . . . . . . 8
![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ∼ 1c k ![_V](rmcv.gif) SIk ∼
![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ∼ 1c k ![_V](rmcv.gif)
![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
7 | | opkex 4113 |
. . . . . . . . . . 11
![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
8 | 7 | elcompl 3225 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ∼ 1c k ![_V](rmcv.gif)
![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) 1c k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | snex 4111 |
. . . . . . . . . . 11
![{](lbrace.gif) ![x](_x.gif)
![_V](rmcv.gif) |
10 | | vex 2862 |
. . . . . . . . . . . 12
![_V](rmcv.gif) |
11 | 10, 9 | opkelxpk 4248 |
. . . . . . . . . . 11
![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) 1c k ![_V](rmcv.gif)
![(](lp.gif) 1c ![{](lbrace.gif) ![x](_x.gif) ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 9, 11 | mpbiran2 885 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) 1c k ![_V](rmcv.gif)
1c![)](rp.gif) |
13 | 8, 12 | xchbinx 301 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ∼ 1c k ![_V](rmcv.gif)
1c![)](rp.gif) |
14 | 13 | orbi1i 506 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ∼
1c
k
![_V](rmcv.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
1c ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
15 | | iman 413 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
1c ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
1c ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | | imor 401 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
1c ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
1c ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | | el1c 4139 |
. . . . . . . . . . . 12
![(](lp.gif) 1c ![E.](exists.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) |
18 | 17 | anbi1i 676 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif)
1c ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | | 19.41v 1901 |
. . . . . . . . . . 11
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 18, 19 | bitr4i 243 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif)
1c ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 20 | notbii 287 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1c ![<<](llangle.gif) ![z](_z.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 15, 16, 21 | 3bitr3i 266 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) 1c ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif)
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 6, 14, 22 | 3bitri 262 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ∼ 1c k ![_V](rmcv.gif) SIk ∼
![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif)
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 23 | albii 1566 |
. . . . . 6
![(](lp.gif) ![A.](forall.gif) ![z](_z.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
∼ 1c k ![_V](rmcv.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![A.](forall.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
25 | | alnex 1543 |
. . . . . . 7
![(](lp.gif) ![A.](forall.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![z](_z.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
26 | | excom 1741 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
27 | | snex 4111 |
. . . . . . . . . . 11
![{](lbrace.gif) ![y](_y.gif)
![_V](rmcv.gif) |
28 | | opkeq1 4059 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![>>](rrangle.gif) ![)](rp.gif) |
29 | 28 | eleq1d 2419 |
. . . . . . . . . . . . 13
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
30 | | vex 2862 |
. . . . . . . . . . . . . . 15
![_V](rmcv.gif) |
31 | 30, 3 | opksnelsik 4265 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif)
∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | | opkex 4113 |
. . . . . . . . . . . . . . 15
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif)
![_V](rmcv.gif) |
33 | 32 | elcompl 3225 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif)
![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 31, 33 | bitri 240 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 29, 34 | syl6bb 252 |
. . . . . . . . . . . 12
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 35 | notbid 285 |
. . . . . . . . . . 11
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![<<](llangle.gif) ![y](_y.gif)
![x](_x.gif) ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 27, 36 | ceqsexv 2894 |
. . . . . . . . . 10
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | | elin 3219 |
. . . . . . . . . . 11
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | | notnot 282 |
. . . . . . . . . . 11
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![<<](llangle.gif) ![y](_y.gif)
![x](_x.gif) ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
40 | 30, 3 | opkelxpk 4248 |
. . . . . . . . . . . . 13
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![(](lp.gif) k ![_V](rmcv.gif)
![(](lp.gif) ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 3, 40 | mpbiran2 885 |
. . . . . . . . . . . 12
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![(](lp.gif) k ![_V](rmcv.gif)
![B](_cb.gif) ![)](rp.gif) |
42 | 41 | anbi2i 675 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif)
![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 38, 39, 42 | 3bitr3i 266 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif)
k
![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
44 | 37, 43 | bitri 240 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 44 | exbii 1582 |
. . . . . . . 8
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
46 | 26, 45 | bitri 240 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![z](_z.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 25, 46 | xchbinx 301 |
. . . . . 6
![(](lp.gif) ![A.](forall.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
48 | 5, 24, 47 | 3bitri 262 |
. . . . 5
![(](lp.gif) P6 ∼ 1c k ![_V](rmcv.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 48 | con2bii 322 |
. . . 4
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif) ![B](_cb.gif) P6 ∼ 1c k ![_V](rmcv.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
50 | 1, 2, 49 | 3bitri 262 |
. . 3
![(](lp.gif) ![E.](exists.gif)
![<<](llangle.gif) ![y](_y.gif) ![x](_x.gif)
P6 ∼ 1c k ![_V](rmcv.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 3 | elimak 4259 |
. . 3
![(](lp.gif) ![(](lp.gif) ![A](_ca.gif) k![B](_cb.gif) ![E.](exists.gif) ![<<](llangle.gif) ![y](_y.gif)
![x](_x.gif) ![A](_ca.gif) ![)](rp.gif) |
52 | 3 | elcompl 3225 |
. . 3
![(](lp.gif) ∼ P6 ∼ 1c k ![_V](rmcv.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) P6 ∼ 1c k ![_V](rmcv.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
53 | 50, 51, 52 | 3bitr4i 268 |
. 2
![(](lp.gif) ![(](lp.gif) ![A](_ca.gif) k![B](_cb.gif) ∼
P6 ∼ 1c k ![_V](rmcv.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
54 | 53 | eqriv 2350 |
1
![(](lp.gif) ![A](_ca.gif) k![B](_cb.gif)
∼ P6 ∼ 1c k ![_V](rmcv.gif)
SIk ∼ ![(](lp.gif) ![(](lp.gif) k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |