Description: Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018) (Proof shortened by Wolf Lammen, 15-May-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | rexdifpr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anass | |
|
2 | eldifpr | |
|
3 | 3anass | |
|
4 | 2 3 | bitri | |
5 | 4 | anbi1i | |
6 | df-3an | |
|
7 | 6 | anbi2i | |
8 | 1 5 7 | 3bitr4i | |
9 | 8 | rexbii2 | |