Step | Hyp | Ref
| Expression |
1 | | bren 6649 |
. . 3
![( (](lp.gif)
![E. E.](exists.gif) ![f
f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) ![) )](rp.gif) |
2 | | f1odm 5379 |
. . . . . . 7
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![A A](_ca.gif) ![) )](rp.gif) |
3 | | vex 2692 |
. . . . . . . 8
![_V
_V](rmcv.gif) |
4 | 3 | dmex 4813 |
. . . . . . 7
![_V _V](rmcv.gif) |
5 | 2, 4 | eqeltrrdi 2232 |
. . . . . 6
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
6 | | pwexg 4112 |
. . . . . 6
![( (](lp.gif) ![~P ~P](scrp.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
7 | | inex1g 4072 |
. . . . . 6
![( (](lp.gif) ![~P ~P](scrp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
8 | 5, 6, 7 | 3syl 17 |
. . . . 5
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
9 | | f1ofo 5382 |
. . . . . . . 8
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-onto-> -onto->](onto.gif) ![B B](_cb.gif) ![) )](rp.gif) |
10 | | forn 5356 |
. . . . . . . 8
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-onto-> -onto->](onto.gif)
![B B](_cb.gif) ![)
)](rp.gif) |
11 | 9, 10 | syl 14 |
. . . . . . 7
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![B B](_cb.gif) ![) )](rp.gif) |
12 | 3 | rnex 4814 |
. . . . . . 7
![_V _V](rmcv.gif) |
13 | 11, 12 | eqeltrrdi 2232 |
. . . . . 6
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
14 | | pwexg 4112 |
. . . . . 6
![( (](lp.gif) ![~P ~P](scrp.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
15 | | inex1g 4072 |
. . . . . 6
![( (](lp.gif) ![~P ~P](scrp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
16 | 13, 14, 15 | 3syl 17 |
. . . . 5
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
17 | | f1of1 5374 |
. . . . . . . . . . 11
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![) )](rp.gif) |
18 | 17 | adantr 274 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![f
f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif) ![)
)](rp.gif) |
19 | 13 | adantr 274 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif)
![_V _V](rmcv.gif) ![) )](rp.gif) |
20 | | simpr 109 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif)
![A A](_ca.gif) ![) )](rp.gif) |
21 | | vex 2692 |
. . . . . . . . . . 11
![_V
_V](rmcv.gif) |
22 | 21 | a1i 9 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) |
23 | | f1imaen2g 6695 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif) ![_V _V](rmcv.gif) ![( (](lp.gif) ![_V _V](rmcv.gif) ![) )](rp.gif) ![( (](lp.gif) ![f
f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![y y](_y.gif) ![) )](rp.gif) |
24 | 18, 19, 20, 22, 23 | syl22anc 1218 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![(
(](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif)
![y y](_y.gif) ![) )](rp.gif) |
25 | | entr 6686 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif)
![C C](_cc.gif) ![(
(](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif)
![C C](_cc.gif) ![) )](rp.gif) |
26 | 24, 25 | sylan 281 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![A A](_ca.gif) ![C C](_cc.gif)
![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![C C](_cc.gif) ![) )](rp.gif) |
27 | 26 | expl 376 |
. . . . . . 7
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![(
(](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif)
![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) |
28 | | imassrn 4900 |
. . . . . . . . 9
![( (](lp.gif) ![f f](_f.gif) !["
"](backquote.gif) ![y y](_y.gif) ![f f](_f.gif) |
29 | 28, 10 | sseqtrid 3152 |
. . . . . . . 8
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-onto-> -onto->](onto.gif) ![(
(](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif)
![B B](_cb.gif) ![) )](rp.gif) |
30 | 9, 29 | syl 14 |
. . . . . . 7
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![B B](_cb.gif) ![) )](rp.gif) |
31 | 27, 30 | jctild 314 |
. . . . . 6
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![(
(](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y
y](_y.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif)
![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
32 | | elin 3264 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![(
(](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
33 | 21 | elpw 3521 |
. . . . . . . 8
![( (](lp.gif) ![~P ~P](scrp.gif)
![A A](_ca.gif) ![) )](rp.gif) |
34 | | breq1 3940 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
35 | 21, 34 | elab 2832 |
. . . . . . . 8
![( (](lp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) |
36 | 33, 35 | anbi12i 456 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif)
![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) |
37 | 32, 36 | bitri 183 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![(
(](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | | elin 3264 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![(
(](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y
y](_y.gif) ![~P ~P](scrp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y
y](_y.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
39 | 3 | imaex 4902 |
. . . . . . . . 9
![( (](lp.gif) ![f f](_f.gif) !["
"](backquote.gif) ![y y](_y.gif) ![_V
_V](rmcv.gif) |
40 | 39 | elpw 3521 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![~P ~P](scrp.gif)
![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![B B](_cb.gif) ![) )](rp.gif) |
41 | | breq1 3940 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y
y](_y.gif) ![( (](lp.gif)
![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
42 | 39, 41 | elab 2832 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![C C](_cc.gif) ![) )](rp.gif) |
43 | 40, 42 | anbi12i 456 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![~P ~P](scrp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) !["
"](backquote.gif) ![y y](_y.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y
y](_y.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) |
44 | 38, 43 | bitri 183 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![(
(](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y
y](_y.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif)
![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) |
45 | 31, 37, 44 | 3imtr4g 204 |
. . . . 5
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f
f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
46 | | f1ocnv 5388 |
. . . . . . 7
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![) )](rp.gif) |
47 | | f1of1 5374 |
. . . . . . . . . . . 12
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-> -1-1->](onetoone.gif) ![A A](_ca.gif) ![) )](rp.gif) |
48 | | f1f1orn 5386 |
. . . . . . . . . . . 12
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-> -1-1->](onetoone.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![) )](rp.gif) |
49 | | f1of1 5374 |
. . . . . . . . . . . 12
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![`' `'](_cnv.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-> -1-1->](onetoone.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![) )](rp.gif) |
50 | 47, 48, 49 | 3syl 17 |
. . . . . . . . . . 11
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-> -1-1->](onetoone.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![) )](rp.gif) |
51 | | vex 2692 |
. . . . . . . . . . . 12
![_V
_V](rmcv.gif) |
52 | 51 | f1imaen 6696 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-> -1-1->](onetoone.gif) ![`' `'](_cnv.gif)
![B B](_cb.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif)
![z z](_z.gif) ![) )](rp.gif) |
53 | 50, 52 | sylan 281 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![B B](_cb.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) !["
"](backquote.gif) ![z z](_z.gif) ![z z](_z.gif) ![) )](rp.gif) |
54 | | entr 6686 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z
z](_z.gif)
![C C](_cc.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) !["
"](backquote.gif) ![z z](_z.gif) ![C C](_cc.gif) ![) )](rp.gif) |
55 | 53, 54 | sylan 281 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif)
![C C](_cc.gif) ![) )](rp.gif) |
56 | 55 | expl 376 |
. . . . . . . 8
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![(
(](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
57 | | f1ofo 5382 |
. . . . . . . . 9
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-onto-> -onto->](onto.gif) ![A A](_ca.gif) ![) )](rp.gif) |
58 | | imassrn 4900 |
. . . . . . . . . 10
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif)
![`' `'](_cnv.gif) ![f f](_f.gif) |
59 | | forn 5356 |
. . . . . . . . . 10
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-onto-> -onto->](onto.gif) ![`' `'](_cnv.gif) ![A A](_ca.gif) ![) )](rp.gif) |
60 | 58, 59 | sseqtrid 3152 |
. . . . . . . . 9
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-onto-> -onto->](onto.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z
z](_z.gif) ![A A](_ca.gif) ![)
)](rp.gif) |
61 | 57, 60 | syl 14 |
. . . . . . . 8
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![(
(](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z
z](_z.gif) ![A A](_ca.gif) ![)
)](rp.gif) |
62 | 56, 61 | jctild 314 |
. . . . . . 7
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![(
(](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif)
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif)
![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
63 | 46, 62 | syl 14 |
. . . . . 6
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![(
(](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) !["
"](backquote.gif) ![z z](_z.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) !["
"](backquote.gif) ![z z](_z.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
64 | | elin 3264 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![(
(](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
65 | 51 | elpw 3521 |
. . . . . . . 8
![( (](lp.gif) ![~P ~P](scrp.gif)
![B B](_cb.gif) ![) )](rp.gif) |
66 | | breq1 3940 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
67 | 51, 66 | elab 2832 |
. . . . . . . 8
![( (](lp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) |
68 | 65, 67 | anbi12i 456 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif)
![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) |
69 | 64, 68 | bitri 183 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![(
(](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
70 | | elin 3264 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![~P ~P](scrp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![) )](rp.gif) |
71 | 3 | cnvex 5085 |
. . . . . . . . . 10
![`' `'](_cnv.gif) ![_V _V](rmcv.gif) |
72 | 71 | imaex 4902 |
. . . . . . . . 9
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![_V _V](rmcv.gif) |
73 | 72 | elpw 3521 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![~P ~P](scrp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif)
![A A](_ca.gif) ![) )](rp.gif) |
74 | | breq1 3940 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) !["
"](backquote.gif) ![z z](_z.gif) ![(
(](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif)
![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) |
75 | 72, 74 | elab 2832 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![{ {](lbrace.gif)
![C C](_cc.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif)
![C C](_cc.gif) ![) )](rp.gif) |
76 | 73, 75 | anbi12i 456 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z
z](_z.gif) ![~P ~P](scrp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) !["
"](backquote.gif) ![z z](_z.gif) ![{
{](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![(
(](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) !["
"](backquote.gif) ![z z](_z.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) !["
"](backquote.gif) ![z z](_z.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
77 | 70, 76 | bitri 183 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif)
![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) |
78 | 63, 69, 77 | 3imtr4g 204 |
. . . . 5
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
79 | | simpl 108 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif)
![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif)
![~P ~P](scrp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
80 | 79 | elpwid 3526 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif)
![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif)
![B B](_cb.gif) ![) )](rp.gif) |
81 | 64, 80 | sylbi 120 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![B B](_cb.gif) ![)
)](rp.gif) |
82 | | imaeq2 4885 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) !["
"](backquote.gif) ![z z](_z.gif) ![(
(](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![( (](lp.gif) ![f f](_f.gif) !["
"](backquote.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) !["
"](backquote.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
83 | | f1orel 5378 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![f f](_f.gif) ![) )](rp.gif) |
84 | | dfrel2 4997 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![`' `'](_cnv.gif) ![`' `'](_cnv.gif)
![f f](_f.gif) ![)
)](rp.gif) |
85 | 83, 84 | sylib 121 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![`' `'](_cnv.gif) ![`' `'](_cnv.gif)
![f f](_f.gif) ![) )](rp.gif) |
86 | 85 | imaeq1d 4888 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![( (](lp.gif) ![`' `'](_cnv.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![)
)](rp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
87 | 86 | adantr 274 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![`' `'](_cnv.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) !["
"](backquote.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) !["
"](backquote.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![(
(](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z
z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
88 | 46, 47 | syl 14 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-> -1-1->](onetoone.gif) ![A A](_ca.gif) ![) )](rp.gif) |
89 | | f1imacnv 5392 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![: :](colon.gif) ![B B](_cb.gif) ![-1-1-> -1-1->](onetoone.gif) ![B B](_cb.gif)
![( (](lp.gif) ![`' `'](_cnv.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![)
)](rp.gif) ![z z](_z.gif) ![) )](rp.gif) |
90 | 88, 89 | sylan 281 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![`' `'](_cnv.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) !["
"](backquote.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) !["
"](backquote.gif) ![z z](_z.gif) ![) )](rp.gif) ![z z](_z.gif) ![) )](rp.gif) |
91 | 87, 90 | eqtr3d 2175 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![)
)](rp.gif) ![z z](_z.gif) ![) )](rp.gif) |
92 | 82, 91 | sylan9eqr 2195 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![B B](_cb.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![)
)](rp.gif) ![( (](lp.gif) ![f
f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![z z](_z.gif) ![) )](rp.gif) |
93 | 92 | eqcomd 2146 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![B B](_cb.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![)
)](rp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y
y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) |
94 | 93 | ex 114 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![B B](_cb.gif) ![(
(](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif)
![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
95 | 81, 94 | sylan2 284 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
96 | 95 | adantrl 470 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z
z](_z.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y
y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
97 | | simpl 108 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif)
![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif)
![~P ~P](scrp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
98 | 97 | elpwid 3526 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif)
![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif)
![A A](_ca.gif) ![) )](rp.gif) |
99 | 32, 98 | sylbi 120 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![A A](_ca.gif) ![)
)](rp.gif) |
100 | | imaeq2 4885 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y
y](_y.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![( (](lp.gif) ![f f](_f.gif) !["
"](backquote.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
101 | | f1imacnv 5392 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-> -1-1->](onetoone.gif)
![A A](_ca.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) !["
"](backquote.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y
y](_y.gif) ![) )](rp.gif) ![y y](_y.gif) ![) )](rp.gif) |
102 | 17, 101 | sylan 281 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![(
(](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![(
(](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![)
)](rp.gif) ![y y](_y.gif) ![) )](rp.gif) |
103 | 100, 102 | sylan9eqr 2195 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![A A](_ca.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![) )](rp.gif)
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![y y](_y.gif) ![) )](rp.gif) |
104 | 103 | eqcomd 2146 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![A A](_ca.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![) )](rp.gif)
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) |
105 | 104 | ex 114 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![A A](_ca.gif) ![(
(](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
106 | 99, 105 | sylan2 284 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) !["
"](backquote.gif) ![y y](_y.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
107 | 106 | adantrr 471 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif)
![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
108 | 96, 107 | impbid 128 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z
z](_z.gif)
![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
109 | 108 | ex 114 |
. . . . 5
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif)
![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![`' `'](_cnv.gif) ![f f](_f.gif) ![" "](backquote.gif) ![z z](_z.gif) ![( (](lp.gif) ![f f](_f.gif) ![" "](backquote.gif) ![y y](_y.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
110 | 8, 16, 45, 78, 109 | en3d 6671 |
. . . 4
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif)
![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif)
![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![) )](rp.gif) |
111 | 110 | exlimiv 1578 |
. . 3
![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![~P ~P](scrp.gif)
![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![) )](rp.gif) |
112 | 1, 111 | sylbi 120 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![~P ~P](scrp.gif)
![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif)
![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![C C](_cc.gif) ![} }](rbrace.gif) ![)
)](rp.gif) ![) )](rp.gif) |
113 | | df-pw 3517 |
. . . 4
![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![A A](_ca.gif) ![} }](rbrace.gif) |
114 | 113 | ineq1i 3278 |
. . 3
![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![A A](_ca.gif)
![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
115 | | inab 3349 |
. . 3
![( (](lp.gif) ![{ {](lbrace.gif) ![A A](_ca.gif)
![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![} }](rbrace.gif) |
116 | 114, 115 | eqtri 2161 |
. 2
![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![} }](rbrace.gif) |
117 | | df-pw 3517 |
. . . 4
![~P ~P](scrp.gif) ![{ {](lbrace.gif) ![B B](_cb.gif) ![} }](rbrace.gif) |
118 | 117 | ineq1i 3278 |
. . 3
![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![B B](_cb.gif)
![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
119 | | inab 3349 |
. . 3
![( (](lp.gif) ![{ {](lbrace.gif) ![B B](_cb.gif)
![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![} }](rbrace.gif) |
120 | 118, 119 | eqtri 2161 |
. 2
![( (](lp.gif) ![~P ~P](scrp.gif) ![{ {](lbrace.gif)
![C C](_cc.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![} }](rbrace.gif) |
121 | 112, 116,
120 | 3brtr3g 3969 |
1
![( (](lp.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |