Step | Hyp | Ref
| Expression |
1 | | vex 2862 |
. . . . . . 7
![_V](rmcv.gif) |
2 | 1 | elimak 4259 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) k1c ![E.](exists.gif) 1c ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif)
Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
3 | | el1c 4139 |
. . . . . . . . . 10
![(](lp.gif) 1c ![E.](exists.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) |
4 | 3 | anbi1i 676 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
1c ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif)
Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
5 | | 19.41v 1901 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif)
Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif)
Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
6 | 4, 5 | bitr4i 243 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
1c ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif)
Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
7 | 6 | exbii 1582 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) 1c ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
8 | | df-rex 2620 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif)
1c ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
1c
![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif)
Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | excom 1741 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 7, 8, 9 | 3bitr4i 268 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif)
1c ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 2, 10 | bitri 240 |
. . . . 5
![(](lp.gif) ![(](lp.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) k1c ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif)
Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | snex 4111 |
. . . . . . . 8
![{](lbrace.gif) ![y](_y.gif)
![_V](rmcv.gif) |
13 | | opkeq1 4059 |
. . . . . . . . 9
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![>>](rrangle.gif) ![)](rp.gif) |
14 | 13 | eleq1d 2419 |
. . . . . . . 8
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![x](_x.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 12, 14 | ceqsexv 2894 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif)
Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![x](_x.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
16 | | eldif 3221 |
. . . . . . . 8
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) Sk ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | | vex 2862 |
. . . . . . . . . 10
![_V](rmcv.gif) |
18 | 17, 1 | elssetk 4270 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) Sk ![x](_x.gif) ![)](rp.gif) |
19 | 12, 1 | opkelxpk 4248 |
. . . . . . . . . . . 12
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![(](lp.gif) 1 k ![_V](rmcv.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) 1 ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 1, 19 | mpbiran2 885 |
. . . . . . . . . . 11
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![(](lp.gif) 1 k ![_V](rmcv.gif) ![{](lbrace.gif) ![y](_y.gif) 1 ![A](_ca.gif) ![)](rp.gif) |
21 | | snelpw1 4146 |
. . . . . . . . . . 11
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) 1 ![A](_ca.gif) ![)](rp.gif) |
22 | 20, 21 | bitri 240 |
. . . . . . . . . 10
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![(](lp.gif) 1 k ![_V](rmcv.gif) ![A](_ca.gif) ![)](rp.gif) |
23 | 22 | notbii 287 |
. . . . . . . . 9
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) ![(](lp.gif) 1 k ![_V](rmcv.gif)
![A](_ca.gif) ![)](rp.gif) |
24 | 18, 23 | anbi12i 678 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) Sk ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif)
![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif)
![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
25 | | annim 414 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
![A](_ca.gif) ![(](lp.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 16, 24, 25 | 3bitri 262 |
. . . . . . 7
![(](lp.gif) ![<<](llangle.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![x](_x.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![(](lp.gif)
![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 15, 26 | bitri 240 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif)
Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif)
![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 27 | exbii 1582 |
. . . . 5
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![<<](llangle.gif) ![t](_t.gif) ![x](_x.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) ![E.](exists.gif) ![(](lp.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
29 | | exnal 1574 |
. . . . 5
![(](lp.gif) ![E.](exists.gif) ![(](lp.gif) ![A](_ca.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
30 | 11, 28, 29 | 3bitri 262 |
. . . 4
![(](lp.gif) ![(](lp.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) k1c ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif)
![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 30 | con2bii 322 |
. . 3
![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif) ![A](_ca.gif) ![(](lp.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) k1c![)](rp.gif) ![)](rp.gif) |
32 | 1 | elpw 3728 |
. . . 4
![(](lp.gif) ![~P](scrp.gif) ![A](_ca.gif) ![)](rp.gif) |
33 | | dfss2 3262 |
. . . 4
![(](lp.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif)
![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 32, 33 | bitri 240 |
. . 3
![(](lp.gif) ![~P](scrp.gif) ![A.](forall.gif) ![y](_y.gif) ![(](lp.gif)
![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 1 | elcompl 3225 |
. . 3
![(](lp.gif) ∼ ![(](lp.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) k1c ![(](lp.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) k1c![)](rp.gif) ![)](rp.gif) |
36 | 31, 34, 35 | 3bitr4i 268 |
. 2
![(](lp.gif) ![~P](scrp.gif) ∼ ![(](lp.gif)
Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) k1c![)](rp.gif) ![)](rp.gif) |
37 | 36 | eqriv 2350 |
1
![~P](scrp.gif) ∼ ![(](lp.gif) Sk ![(](lp.gif) 1 k ![_V](rmcv.gif) ![)](rp.gif) ![)](rp.gif) k1c![)](rp.gif) |