Description: Obsolete version of f1eqcocnv as of 29-May-2024. (Contributed by Stefan O'Rear, 12-Feb-2015) (New usage is discouraged.) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | f1eqcocnvOLD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1cocnv1 | |
|
2 | coeq2 | |
|
3 | 2 | eqeq1d | |
4 | 1 3 | syl5ibcom | |
5 | 4 | adantr | |
6 | f1fn | |
|
7 | 6 | adantl | |
8 | 7 | adantr | |
9 | f1fn | |
|
10 | 9 | adantr | |
11 | 10 | adantr | |
12 | equid | |
|
13 | resieq | |
|
14 | 12 13 | mpbiri | |
15 | 14 | anidms | |
16 | 15 | adantl | |
17 | breq | |
|
18 | 17 | ad2antlr | |
19 | 16 18 | mpbird | |
20 | fnfun | |
|
21 | 7 20 | syl | |
22 | fndm | |
|
23 | 7 22 | syl | |
24 | 23 | eleq2d | |
25 | 24 | biimpar | |
26 | funopfvb | |
|
27 | 21 25 26 | syl2an2r | |
28 | 27 | bicomd | |
29 | df-br | |
|
30 | eqcom | |
|
31 | 28 29 30 | 3bitr4g | |
32 | 31 | biimpd | |
33 | df-br | |
|
34 | fnfun | |
|
35 | 10 34 | syl | |
36 | fndm | |
|
37 | 10 36 | syl | |
38 | 37 | eleq2d | |
39 | 38 | biimpar | |
40 | funopfvb | |
|
41 | 35 39 40 | syl2an2r | |
42 | 33 41 | bitr4id | |
43 | vex | |
|
44 | vex | |
|
45 | 43 44 | brcnv | |
46 | eqcom | |
|
47 | 42 45 46 | 3bitr4g | |
48 | 47 | biimpd | |
49 | 32 48 | anim12d | |
50 | 49 | eximdv | |
51 | 44 44 | brco | |
52 | fvex | |
|
53 | 52 | eqvinc | |
54 | 50 51 53 | 3imtr4g | |
55 | 54 | adantlr | |
56 | 19 55 | mpd | |
57 | 8 11 56 | eqfnfvd | |
58 | 57 | eqcomd | |
59 | 58 | ex | |
60 | 5 59 | impbid | |