Description: Define a quantity whose definition involves a choice of representative, but which is uniquely determined regardless of the choice. (Contributed by Jeff Madsen, 1-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | unirep.1 | |
|
unirep.2 | |
||
unirep.3 | |
||
unirep.4 | |
||
unirep.5 | |
||
Assertion | unirep | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unirep.1 | |
|
2 | unirep.2 | |
|
3 | unirep.3 | |
|
4 | unirep.4 | |
|
5 | unirep.5 | |
|
6 | eqidd | |
|
7 | 6 | ancli | |
8 | 2 | eqeq2d | |
9 | 1 8 | anbi12d | |
10 | 9 | rspcev | |
11 | 7 10 | sylan2 | |
12 | 11 | adantl | |
13 | nfcvd | |
|
14 | 13 2 | csbiegf | |
15 | 5 | csbex | |
16 | 14 15 | eqeltrrdi | |
17 | 16 | ad2antrl | |
18 | eqeq1 | |
|
19 | 18 | anbi2d | |
20 | 19 | rexbidv | |
21 | 20 | spcegv | |
22 | 16 21 | syl | |
23 | 22 | adantr | |
24 | 11 23 | mpd | |
25 | 24 | adantl | |
26 | r19.29 | |
|
27 | r19.29 | |
|
28 | an4 | |
|
29 | pm3.35 | |
|
30 | eqeq12 | |
|
31 | 29 30 | syl5ibrcom | |
32 | 31 | ancoms | |
33 | 32 | expimpd | |
34 | 28 33 | syl5bi | |
35 | 34 | ancomsd | |
36 | 35 | expdimp | |
37 | 36 | rexlimivw | |
38 | 37 | imp | |
39 | 27 38 | sylan | |
40 | 39 | an32s | |
41 | 40 | ex | |
42 | 41 | rexlimivw | |
43 | 26 42 | syl | |
44 | 43 | expimpd | |
45 | 44 | adantr | |
46 | 45 | alrimivv | |
47 | eqeq1 | |
|
48 | 47 | anbi2d | |
49 | 48 | rexbidv | |
50 | 4 | eqeq2d | |
51 | 3 50 | anbi12d | |
52 | 51 | cbvrexvw | |
53 | 49 52 | bitrdi | |
54 | 53 | eu4 | |
55 | 25 46 54 | sylanbrc | |
56 | 20 | iota2 | |
57 | 17 55 56 | syl2anc | |
58 | 12 57 | mpbid | |