Description: Lemma for 2reu5 . This lemma is interesting in its own right, showing that existential restriction in the last conjunct (the "at most one" part) is optional; compare rmo2 . (Contributed by Alexander van der Vekens, 17-Jun-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | 2reu5lem3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2reu5lem1 | |
|
2 | 2reu5lem2 | |
|
3 | 1 2 | anbi12i | |
4 | 2eu5 | |
|
5 | 3anass | |
|
6 | 5 | exbii | |
7 | 19.42v | |
|
8 | df-rex | |
|
9 | 8 | bicomi | |
10 | 9 | anbi2i | |
11 | 6 7 10 | 3bitri | |
12 | 11 | exbii | |
13 | df-rex | |
|
14 | 12 13 | bitr4i | |
15 | 3anan12 | |
|
16 | 15 | imbi1i | |
17 | impexp | |
|
18 | impexp | |
|
19 | 18 | imbi2i | |
20 | 16 17 19 | 3bitri | |
21 | 20 | albii | |
22 | df-ral | |
|
23 | r19.21v | |
|
24 | 21 22 23 | 3bitr2i | |
25 | 24 | albii | |
26 | df-ral | |
|
27 | 25 26 | bitr4i | |
28 | 27 | exbii | |
29 | 28 | exbii | |
30 | 14 29 | anbi12i | |
31 | 3 4 30 | 3bitri | |