Step | Hyp | Ref
| Expression |
1 | | nnsucelrlem1 4424 |
. . . 4
![{](lbrace.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![m](_m.gif) ![)](rp.gif) ![_V](rmcv.gif) |
2 | | addceq1 4383 |
. . . . . . . . . 10
![(](lp.gif) 0c ![(](lp.gif)
1c
0c 1c![)](rp.gif) ![)](rp.gif) |
3 | | addcid2 4407 |
. . . . . . . . . 10
0c
1c
1c |
4 | 2, 3 | syl6eq 2401 |
. . . . . . . . 9
![(](lp.gif) 0c ![(](lp.gif)
1c
1c![)](rp.gif) |
5 | 4 | eleq2d 2420 |
. . . . . . . 8
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) 1c![)](rp.gif) ![)](rp.gif) |
6 | | el1c 4139 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
1c
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) |
7 | 5, 6 | syl6bb 252 |
. . . . . . 7
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
8 | 7 | anbi2d 684 |
. . . . . 6
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif)
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | eleq2 2414 |
. . . . . . 7
![(](lp.gif) 0c ![(](lp.gif)
0c![)](rp.gif) ![)](rp.gif) |
10 | | df-0c 4377 |
. . . . . . . . 9
0c
![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) |
11 | 10 | eleq2i 2417 |
. . . . . . . 8
![(](lp.gif) 0c
![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
12 | | vex 2862 |
. . . . . . . . 9
![_V](rmcv.gif) |
13 | 12 | elsnc 3756 |
. . . . . . . 8
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
14 | 11, 13 | bitri 240 |
. . . . . . 7
![(](lp.gif) 0c
![(/)](varnothing.gif) ![)](rp.gif) |
15 | 9, 14 | syl6bb 252 |
. . . . . 6
![(](lp.gif) 0c ![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 8, 15 | imbi12d 311 |
. . . . 5
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 16 | 2albidv 1627 |
. . . 4
![(](lp.gif) 0c ![(](lp.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![m](_m.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | | addceq1 4383 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
19 | 18 | eleq2d 2420 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 19 | anbi2d 684 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
21 | | eleq2 2414 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 20, 21 | imbi12d 311 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 22 | 2albidv 1627 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![m](_m.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | | eleq12 2415 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif)
![c](_c.gif) ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 24 | ancoms 439 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
![z](_z.gif) ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 25 | notbid 285 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
![z](_z.gif) ![(](lp.gif) ![c](_c.gif) ![)](rp.gif) ![)](rp.gif) |
27 | | sneq 3744 |
. . . . . . . . . 10
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![)](rp.gif) |
28 | | uneq12 3413 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 27, 28 | sylan2 460 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
30 | 29 | eleq1d 2419 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 26, 30 | anbi12d 691 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
![z](_z.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif)
![(](lp.gif)
![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | | eleq1 2413 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 32 | adantr 451 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
![z](_z.gif) ![(](lp.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 31, 33 | imbi12d 311 |
. . . . . 6
![(](lp.gif) ![(](lp.gif)
![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 34 | cbval2v 2006 |
. . . . 5
![(](lp.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 23, 35 | syl6bb 252 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![m](_m.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | | addceq1 4383 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
1c
1c![)](rp.gif) ![)](rp.gif) |
38 | 37 | eleq2d 2420 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) 1c 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 38 | anbi2d 684 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![(](lp.gif)
![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif)
1c
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
40 | | eleq2 2414 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 39, 40 | imbi12d 311 |
. . . . 5
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif)
1c
1c![)](rp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
42 | 41 | 2albidv 1627 |
. . . 4
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![m](_m.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif)
1c
1c![)](rp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
43 | | addceq1 4383 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
44 | 43 | eleq2d 2420 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 44 | anbi2d 684 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
46 | | eleq2 2414 |
. . . . . 6
![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 45, 46 | imbi12d 311 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![m](_m.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
48 | 47 | 2albidv 1627 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![m](_m.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
49 | | vex 2862 |
. . . . . . . . . . 11
![_V](rmcv.gif) |
50 | 49 | unsneqsn 3887 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 50 | ord 366 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
52 | 49 | snid 3760 |
. . . . . . . . . 10
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) |
53 | | eleq2 2414 |
. . . . . . . . . 10
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
54 | 52, 53 | mpbiri 224 |
. . . . . . . . 9
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![a](_a.gif) ![)](rp.gif) |
55 | 51, 54 | syl6 29 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
56 | 55 | con1d 116 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
57 | 56 | exlimiv 1634 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
58 | 57 | impcom 419 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
59 | 58 | gen2 1547 |
. . . 4
![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
60 | | elsuc 4413 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif)
1c
1c
![E.](exists.gif) ![(](lp.gif)
1c![)](rp.gif) ![E.](exists.gif) ∼ ![b](_b.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
61 | | vex 2862 |
. . . . . . . . . . . . 13
![_V](rmcv.gif) |
62 | 61 | elcompl 3225 |
. . . . . . . . . . . 12
![(](lp.gif) ∼ ![b](_b.gif) ![)](rp.gif) |
63 | 62 | anbi2i 675 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ∼ ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
1c
![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
64 | | simprrl 740 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
65 | | sneq 3744 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) |
66 | 65 | adantr 451 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) |
67 | 64, 66 | difeq12d 3386 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
68 | | simprrr 741 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![a](_a.gif) ![)](rp.gif) |
69 | | nnsucelrlem2 4425 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) |
70 | 68, 69 | syl 15 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) |
71 | | simprlr 739 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![b](_b.gif) ![)](rp.gif) |
72 | | nnsucelrlem2 4425 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![b](_b.gif) ![)](rp.gif) |
73 | 71, 72 | syl 15 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![b](_b.gif) ![)](rp.gif) |
74 | 67, 70, 73 | 3eqtr3d 2393 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![b](_b.gif) ![)](rp.gif) |
75 | | simprll 738 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
76 | 74, 75 | eqeltrd 2427 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
77 | 76 | 3adantr1 1114 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
78 | 77 | ex 423 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
79 | | simpl 443 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![y](_y.gif) ![)](rp.gif) |
80 | | simpr3l 1016 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
81 | | simpr2r 1015 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![b](_b.gif) ![)](rp.gif) |
82 | 49 | nnsucelrlem3 4426 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![b](_b.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
83 | 79, 80, 81, 82 | syl3anc 1182 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
84 | | simp22r 1075 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![b](_b.gif) ![)](rp.gif) |
85 | | difsn 3845 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![a](_a.gif) ![)](rp.gif) |
86 | 85 | uneq1d 3417 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
87 | 86 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
88 | 87 | biimpcd 215 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
89 | 88 | 3ad2ant3 978 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
90 | | simp23l 1076 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
91 | 90 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
92 | 61 | snss 3838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![b](_b.gif) ![)](rp.gif) |
93 | | ssequn2 3436 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![b](_b.gif) ![)](rp.gif) |
94 | 92, 93 | bitr2i 241 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![b](_b.gif) ![)](rp.gif) |
95 | 94 | biimpi 186 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![b](_b.gif) ![)](rp.gif) |
96 | 95 | eqcoms 2356 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![b](_b.gif) ![)](rp.gif) |
97 | 91, 96 | syl6bi 219 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
98 | 89, 97 | syld 40 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![(](lp.gif)
![b](_b.gif) ![)](rp.gif) ![)](rp.gif) |
99 | 84, 98 | mt3d 117 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![a](_a.gif) ![)](rp.gif) |
100 | | nnsucelrlem4 4427 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![a](_a.gif) ![)](rp.gif) |
101 | 99, 100 | syl 15 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![a](_a.gif) ![)](rp.gif) |
102 | | simpl3r 1011 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![a](_a.gif) ![)](rp.gif) |
103 | | difss 3393 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) |
104 | 103 | sseli 3269 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![a](_a.gif) ![)](rp.gif) |
105 | 102, 104 | nsyl 113 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
106 | | simp2l 981 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
107 | | eleq1 2413 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
108 | 107 | biimpd 198 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
109 | 106, 108 | mpan9 455 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
110 | | simpl1 958 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
111 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . 23
![{](lbrace.gif) ![y](_y.gif)
![_V](rmcv.gif) |
112 | 12, 111 | difex 4107 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![_V](rmcv.gif) |
113 | | eleq12 2415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
114 | 113 | ancoms 439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
115 | 114 | notbid 285 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![x](_x.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
116 | | sneq 3744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) |
117 | | uneq12 3413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![z](_z.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
118 | 116, 117 | sylan2 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![x](_x.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
119 | 118 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
120 | 115, 119 | anbi12d 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
121 | | eleq1 2413 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif)
![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
122 | 121 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . 24
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
123 | 120, 122 | imbi12d 311 |
. . . . . . . . . . . . . . . . . . . . . . 23
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
124 | 123 | spc2gv 2942 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![_V](rmcv.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
125 | 112, 49, 124 | mp2an 653 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
126 | 110, 125 | syl 15 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
127 | 105, 109,
126 | mp2and 660 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![n](_n.gif) ![)](rp.gif) |
128 | 127 | 3adant1 973 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![n](_n.gif) ![)](rp.gif) |
129 | 61 | snid 3760 |
. . . . . . . . . . . . . . . . . . . . 21
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) |
130 | | eldif 3221 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
131 | 130 | simprbi 450 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) |
132 | 129, 131 | mt2 170 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) |
133 | 61 | elcompl 3225 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ∼ ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
134 | 132, 133 | mpbir 200 |
. . . . . . . . . . . . . . . . . . 19
∼ ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) |
135 | | eqid 2353 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) |
136 | | sneq 3744 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![{](lbrace.gif) ![w](_w.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) |
137 | 136 | uneq2d 3418 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
138 | 137 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
139 | 138 | rspcev 2955 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ∼
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![E.](exists.gif)
∼ ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
140 | 134, 135,
139 | mp2an 653 |
. . . . . . . . . . . . . . . . . 18
![E.](exists.gif) ∼ ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![)](rp.gif) |
141 | | compleq 3243 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ∼
∼ ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
142 | | uneq1 3411 |
. . . . . . . . . . . . . . . . . . . . . 22
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif)
![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
143 | 142 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . . 21
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
144 | 141, 143 | rexeqbidv 2820 |
. . . . . . . . . . . . . . . . . . . 20
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![E.](exists.gif) ∼ ![d](_d.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif)
![E.](exists.gif) ∼ ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
145 | 144 | rspcev 2955 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![E.](exists.gif) ∼ ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![)](rp.gif) ![E.](exists.gif) ![E.](exists.gif)
∼ ![d](_d.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
146 | | elsuc 4413 |
. . . . . . . . . . . . . . . . . . 19
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif)
1c
![E.](exists.gif)
![E.](exists.gif) ∼ ![d](_d.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
147 | 145, 146 | sylibr 203 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![E.](exists.gif) ∼ ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![w](_w.gif) ![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
148 | 128, 140,
147 | sylancl 643 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
149 | 101, 148 | eqeltrrd 2428 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![)](rp.gif)
![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
150 | 83, 149 | mpd3an3 1278 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
151 | 150 | ex 423 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
152 | 78, 151 | pm2.61ine 2592 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![a](_a.gif) ![)](rp.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
153 | 152 | 3expa 1151 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![a](_a.gif) ![)](rp.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
154 | 153 | exp32 588 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ![b](_b.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
155 | 63, 154 | sylan2b 461 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![(](lp.gif)
![(](lp.gif) 1c ∼ ![b](_b.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![(](lp.gif)
![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
156 | 155 | rexlimdvva 2745 |
. . . . . . . . 9
![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) ![E.](exists.gif)
![(](lp.gif) 1c![)](rp.gif) ![E.](exists.gif) ∼ ![b](_b.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif)
![(](lp.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
157 | 60, 156 | syl5bi 208 |
. . . . . . . 8
![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![(](lp.gif)
1c
1c
![(](lp.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
158 | 157 | com23 72 |
. . . . . . 7
![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif)
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif) 1c 1c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
159 | 158 | imp3a 420 |
. . . . . 6
![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif)
1c
1c![)](rp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
160 | 159 | alrimivv 1632 |
. . . . 5
![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![n](_n.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif)
1c
1c![)](rp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
161 | 160 | a1i 10 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) ![A.](forall.gif) ![c](_c.gif) ![A.](forall.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![n](_n.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif) ![(](lp.gif)
1c
1c![)](rp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
162 | 1, 17, 36, 42, 48, 59, 161 | finds 4411 |
. . 3
![(](lp.gif) Nn ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
163 | | nnsucelr.2 |
. . . . 5
![_V](rmcv.gif) |
164 | | eleq1 2413 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
165 | 164 | notbid 285 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
![a](_a.gif) ![)](rp.gif) ![)](rp.gif) |
166 | | sneq 3744 |
. . . . . . . . 9
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif) ![)](rp.gif) |
167 | 166 | uneq2d 3418 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
168 | 167 | eleq1d 2419 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c ![(](lp.gif) ![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
169 | 165, 168 | anbi12d 691 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
170 | 169 | imbi1d 308 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![M](_cm.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
171 | 163, 170 | spcv 2945 |
. . . 4
![(](lp.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![M](_cm.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
172 | 171 | alimi 1559 |
. . 3
![(](lp.gif) ![A.](forall.gif) ![a](_a.gif) ![A.](forall.gif) ![x](_x.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![x](_x.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![M](_cm.gif) ![A.](forall.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
173 | | nnsucelr.1 |
. . . 4
![_V](rmcv.gif) |
174 | | eleq2 2414 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
175 | 174 | notbid 285 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
176 | | uneq1 3411 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif)
![(](lp.gif) ![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
177 | 176 | eleq1d 2419 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif)
![(](lp.gif) 1c ![(](lp.gif) ![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
178 | 175, 177 | anbi12d 691 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
179 | | eleq1 2413 |
. . . . 5
![(](lp.gif) ![(](lp.gif)
![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
180 | 178, 179 | imbi12d 311 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![M](_cm.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
181 | 173, 180 | spcv 2945 |
. . 3
![(](lp.gif) ![A.](forall.gif) ![a](_a.gif) ![(](lp.gif) ![(](lp.gif)
![(](lp.gif) ![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![M](_cm.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif) ![(](lp.gif)
1c![)](rp.gif) ![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
182 | 162, 172,
181 | 3syl 18 |
. 2
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif)
![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
183 | 182 | imp 418 |
1
![(](lp.gif) ![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![X](_cx.gif) ![}](rbrace.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![M](_cm.gif) ![)](rp.gif) |