Step | Hyp | Ref
| Expression |
1 | | snex 4111 |
. . . . 5
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
2 | | opkeq1 4059 |
. . . . . 6
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) ![>>](rrangle.gif) ![)](rp.gif) |
3 | 2 | eleq1d 2419 |
. . . . 5
![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
4 | 1, 3 | ceqsexv 2894 |
. . . 4
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k Sk ![)](rp.gif)
![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) ![)](rp.gif) |
5 | | elin 3219 |
. . . . 5
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k Sk ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k
Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins2k Sk ![)](rp.gif) ![)](rp.gif) |
6 | | snex 4111 |
. . . . . . . 8
![{](lbrace.gif) ![x](_x.gif)
![_V](rmcv.gif) |
7 | | ndisjrelk.1 |
. . . . . . . 8
![_V](rmcv.gif) |
8 | | ndisjrelk.2 |
. . . . . . . 8
![_V](rmcv.gif) |
9 | 6, 7, 8 | otkelins3k 4256 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif)
Ins3k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![A](_ca.gif) Sk ![)](rp.gif) |
10 | | vex 2862 |
. . . . . . . 8
![_V](rmcv.gif) |
11 | 10, 7 | elssetk 4270 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![A](_ca.gif) Sk ![A](_ca.gif) ![)](rp.gif) |
12 | 9, 11 | bitri 240 |
. . . . . 6
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif)
Ins3k Sk ![A](_ca.gif) ![)](rp.gif) |
13 | 6, 7, 8 | otkelins2k 4255 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif)
Ins2k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![B](_cb.gif) Sk ![)](rp.gif) |
14 | 10, 8 | elssetk 4270 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![B](_cb.gif) Sk ![B](_cb.gif) ![)](rp.gif) |
15 | 13, 14 | bitri 240 |
. . . . . 6
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif)
Ins2k Sk ![B](_cb.gif) ![)](rp.gif) |
16 | 12, 15 | anbi12i 678 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins2k Sk ![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 5, 16 | bitri 240 |
. . . 4
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k Sk ![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
18 | 4, 17 | bitri 240 |
. . 3
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k Sk ![)](rp.gif)
![(](lp.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 18 | exbii 1582 |
. 2
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k Sk ![)](rp.gif)
![E.](exists.gif) ![x](_x.gif) ![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
20 | | opkex 4113 |
. . . 4
![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![_V](rmcv.gif) |
21 | 20 | elimak 4259 |
. . 3
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![E.](exists.gif) 1 1 1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k Sk ![)](rp.gif) ![)](rp.gif) |
22 | | elpw121c 4148 |
. . . . . . 7
![(](lp.gif) 1 1 1c ![E.](exists.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![)](rp.gif) |
23 | 22 | anbi1i 676 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k Sk ![)](rp.gif)
![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | | 19.41v 1901 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k Sk ![)](rp.gif)
![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 23, 24 | bitr4i 243 |
. . . . 5
![(](lp.gif) ![(](lp.gif) 1 1
1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k Sk ![)](rp.gif)
![E.](exists.gif) ![x](_x.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 25 | exbii 1582 |
. . . 4
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k Sk ![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
27 | | df-rex 2620 |
. . . 4
![(](lp.gif) ![E.](exists.gif)
1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k Sk ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1 1 1c ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
28 | | excom 1741 |
. . . 4
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif)
![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k Sk ![)](rp.gif)
![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif)
Ins3k Sk Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 26, 27, 28 | 3bitr4i 268 |
. . 3
![(](lp.gif) ![E.](exists.gif)
1 1
1c![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k Sk ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
30 | 21, 29 | bitri 240 |
. 2
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![E.](exists.gif) ![x](_x.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![{](lbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![}](rbrace.gif) ![<<](llangle.gif) ![t](_t.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>>](rrangle.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
31 | | n0 3559 |
. . 3
![(](lp.gif) ![(](lp.gif) ![B](_cb.gif)
![E.](exists.gif)
![(](lp.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
32 | | elin 3219 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![B](_cb.gif)
![(](lp.gif) ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 32 | exbii 1582 |
. . 3
![(](lp.gif) ![E.](exists.gif)
![(](lp.gif) ![B](_cb.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 31, 33 | bitri 240 |
. 2
![(](lp.gif) ![(](lp.gif) ![B](_cb.gif)
![E.](exists.gif) ![x](_x.gif) ![(](lp.gif)
![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 19, 30, 34 | 3bitr4i 268 |
1
![(](lp.gif) ![<<](llangle.gif) ![A](_ca.gif) ![B](_cb.gif) ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) ![B](_cb.gif) ![(/)](varnothing.gif) ![)](rp.gif) |