Step | Hyp | Ref
| Expression |
1 | | elima1c 4947 |
. . . 4
![(](lp.gif) ![<.](langle.gif) ![A](_ca.gif)
![B](_cb.gif) ![(](lp.gif) Ins2 S Ins3 S SI ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) 1c ![E.](exists.gif) ![x](_x.gif) ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![<.](langle.gif) ![A](_ca.gif)
![B](_cb.gif) ![>.](rangle.gif)
Ins2 S Ins3 S SI ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
2 | | elsymdif 3223 |
. . . . . 6
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![<.](langle.gif) ![A](_ca.gif)
![B](_cb.gif) ![>.](rangle.gif)
Ins2 S Ins3 S SI ![R](_cr.gif) ![)](rp.gif)
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>.](rangle.gif) Ins2
S ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>.](rangle.gif) Ins3 S SI ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
3 | | brimage.1 |
. . . . . . . . 9
![_V](rmcv.gif) |
4 | 3 | otelins2 5791 |
. . . . . . . 8
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![<.](langle.gif) ![A](_ca.gif)
![B](_cb.gif) ![>.](rangle.gif) Ins2
S ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![B](_cb.gif) S ![)](rp.gif) |
5 | | vex 2862 |
. . . . . . . . 9
![_V](rmcv.gif) |
6 | | brimage.2 |
. . . . . . . . 9
![_V](rmcv.gif) |
7 | 5, 6 | opelssetsn 4760 |
. . . . . . . 8
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![B](_cb.gif) S ![B](_cb.gif) ![)](rp.gif) |
8 | 4, 7 | bitri 240 |
. . . . . . 7
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![<.](langle.gif) ![A](_ca.gif)
![B](_cb.gif) ![>.](rangle.gif) Ins2
S ![B](_cb.gif) ![)](rp.gif) |
9 | 6 | otelins3 5792 |
. . . . . . . 8
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![<.](langle.gif) ![A](_ca.gif)
![B](_cb.gif) ![>.](rangle.gif) Ins3 S SI ![R](_cr.gif) ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![A](_ca.gif) S
SI ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) |
10 | | brcnv 4892 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SI ![R](_cr.gif) SI
![R](_cr.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) |
11 | 5 | brsnsi2 5776 |
. . . . . . . . . . . . . 14
![(](lp.gif) SI ![R](_cr.gif) ![{](lbrace.gif) ![x](_x.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 10, 11 | bitri 240 |
. . . . . . . . . . . . 13
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SI ![R](_cr.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
13 | 12 | anbi1i 676 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SI ![R](_cr.gif) S ![A](_ca.gif)
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) S ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | 19.41v 1901 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) S ![A](_ca.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) S
![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 13, 14 | bitr4i 243 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SI ![R](_cr.gif) S ![A](_ca.gif)
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) S ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 15 | exbii 1582 |
. . . . . . . . . 10
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SI ![R](_cr.gif) S ![A](_ca.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) S ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
17 | | excom 1741 |
. . . . . . . . . 10
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) S
![A](_ca.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) S ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
18 | | anass 630 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) S ![A](_ca.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) ![y](_y.gif) ![R](_cr.gif) S ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 18 | exbii 1582 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) S ![A](_ca.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) ![y](_y.gif) ![R](_cr.gif) S ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | | snex 4111 |
. . . . . . . . . . . . 13
![{](lbrace.gif) ![y](_y.gif)
![_V](rmcv.gif) |
21 | | breq1 4642 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) S ![{](lbrace.gif) ![y](_y.gif) S ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 21 | anbi2d 684 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![R](_cr.gif) S
![A](_ca.gif) ![(](lp.gif) ![y](_y.gif) ![R](_cr.gif) ![{](lbrace.gif) ![y](_y.gif) S ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | | ancom 437 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![R](_cr.gif) ![{](lbrace.gif) ![y](_y.gif) S ![A](_ca.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) S ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
24 | | vex 2862 |
. . . . . . . . . . . . . . . . 17
![_V](rmcv.gif) |
25 | 24, 3 | brssetsn 4759 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) S ![A](_ca.gif) ![)](rp.gif) |
26 | 25 | anbi1i 676 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) S
![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) ![(](lp.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 23, 26 | bitri 240 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![R](_cr.gif) ![{](lbrace.gif) ![y](_y.gif) S ![A](_ca.gif) ![(](lp.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 22, 27 | syl6bb 252 |
. . . . . . . . . . . . 13
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![R](_cr.gif) S
![A](_ca.gif) ![(](lp.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 20, 28 | ceqsexv 2894 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) ![y](_y.gif) ![R](_cr.gif) S ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
30 | 19, 29 | bitri 240 |
. . . . . . . . . . 11
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) S ![A](_ca.gif) ![(](lp.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 30 | exbii 1582 |
. . . . . . . . . 10
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) S
![A](_ca.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 16, 17, 31 | 3bitri 262 |
. . . . . . . . 9
![(](lp.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SI ![R](_cr.gif) S ![A](_ca.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
33 | | opelco 4884 |
. . . . . . . . 9
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![A](_ca.gif) S SI ![R](_cr.gif) ![E.](exists.gif) ![t](_t.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) SI ![R](_cr.gif) S ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
34 | | elima2 4755 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif)
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![y](_y.gif) ![R](_cr.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 32, 33, 34 | 3bitr4i 268 |
. . . . . . . 8
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![A](_ca.gif) S SI ![R](_cr.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 9, 35 | bitri 240 |
. . . . . . 7
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![<.](langle.gif) ![A](_ca.gif)
![B](_cb.gif) ![>.](rangle.gif) Ins3 S SI ![R](_cr.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 8, 36 | bibi12i 306 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>.](rangle.gif) Ins2
S ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>.](rangle.gif) Ins3 S SI ![R](_cr.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 2, 37 | xchbinx 301 |
. . . . 5
![(](lp.gif) ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![<.](langle.gif) ![A](_ca.gif)
![B](_cb.gif) ![>.](rangle.gif)
Ins2 S Ins3 S SI ![R](_cr.gif) ![)](rp.gif)
![(](lp.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 38 | exbii 1582 |
. . . 4
![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![<.](langle.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) ![>.](rangle.gif) Ins2 S Ins3 S SI ![R](_cr.gif) ![)](rp.gif)
![E.](exists.gif) ![(](lp.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
40 | | exnal 1574 |
. . . 4
![(](lp.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 1, 39, 40 | 3bitri 262 |
. . 3
![(](lp.gif) ![<.](langle.gif) ![A](_ca.gif)
![B](_cb.gif) ![(](lp.gif) Ins2 S Ins3 S SI ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) 1c ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
42 | 41 | con2bii 322 |
. 2
![(](lp.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![<.](langle.gif) ![A](_ca.gif)
![B](_cb.gif) ![(](lp.gif) Ins2 S Ins3 S SI ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) |
43 | | dfcleq 2347 |
. 2
![(](lp.gif) ![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif)
![A.](forall.gif) ![x](_x.gif) ![(](lp.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
44 | | df-image 5754 |
. . . 4
Image ∼ ![(](lp.gif) Ins2 S
Ins3 S SI ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif) |
45 | 44 | breqi 4645 |
. . 3
![(](lp.gif) Image![R](_cr.gif)
∼ ![(](lp.gif) Ins2 S Ins3 S SI ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif) ![B](_cb.gif) ![)](rp.gif) |
46 | | df-br 4640 |
. . 3
![(](lp.gif) ∼ ![(](lp.gif)
Ins2 S Ins3 S SI ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif) ![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) ∼ ![(](lp.gif) Ins2 S
Ins3 S SI ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) |
47 | 3, 6 | opex 4588 |
. . . 4
![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) ![_V](rmcv.gif) |
48 | 47 | elcompl 3225 |
. . 3
![(](lp.gif) ![<.](langle.gif) ![A](_ca.gif)
![B](_cb.gif) ∼ ![(](lp.gif) Ins2 S Ins3 S SI ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) 1c ![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) ![(](lp.gif) Ins2 S
Ins3 S SI ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) |
49 | 45, 46, 48 | 3bitri 262 |
. 2
![(](lp.gif) Image![R](_cr.gif)
![<.](langle.gif) ![A](_ca.gif) ![B](_cb.gif) ![(](lp.gif) Ins2 S
Ins3 S SI ![R](_cr.gif) ![)](rp.gif) ![)](rp.gif) 1c![)](rp.gif) ![)](rp.gif) |
50 | 42, 43, 49 | 3bitr4ri 269 |
1
![(](lp.gif) Image![R](_cr.gif)
![(](lp.gif) ![R](_cr.gif) !["](backquote.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |