Description: Double restricted existential uniqueness, analogous to 2eu3 . (Contributed by Alexander van der Vekens, 29-Jun-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | 2reu3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcom | |
|
2 | 1 | ralbii | |
3 | nfrmo1 | |
|
4 | 3 | r19.32 | |
5 | 2 4 | bitri | |
6 | orcom | |
|
7 | 5 6 | bitri | |
8 | 7 | ralbii | |
9 | nfcv | |
|
10 | nfrmo1 | |
|
11 | 9 10 | nfralw | |
12 | 11 | r19.32 | |
13 | 8 12 | bitri | |
14 | 2reu1 | |
|
15 | 14 | biimpd | |
16 | ancom | |
|
17 | 15 16 | imbitrdi | |
18 | 17 | adantld | |
19 | 2reu1 | |
|
20 | 19 | biimpd | |
21 | 20 | adantrd | |
22 | 18 21 | jaoi | |
23 | 2rexreu | |
|
24 | 2rexreu | |
|
25 | 24 | ancoms | |
26 | 23 25 | jca | |
27 | 22 26 | impbid1 | |
28 | 13 27 | sylbi | |