Description: Introduce or eliminate a disjunct in a unique existential quantifier. (Contributed by NM, 21-Oct-2005) (Proof shortened by Andrew Salmon, 9-Jul-2011) (Proof shortened by Wolf Lammen, 27-Dec-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | euor2 | |- ( -. E. x ph -> ( E! x ( ph \/ ps ) <-> E! x ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfe1 | |- F/ x E. x ph |
|
| 2 | 1 | nfn | |- F/ x -. E. x ph |
| 3 | 19.8a | |- ( ph -> E. x ph ) |
|
| 4 | biorf | |- ( -. ph -> ( ps <-> ( ph \/ ps ) ) ) |
|
| 5 | 4 | bicomd | |- ( -. ph -> ( ( ph \/ ps ) <-> ps ) ) |
| 6 | 3 5 | nsyl5 | |- ( -. E. x ph -> ( ( ph \/ ps ) <-> ps ) ) |
| 7 | 2 6 | eubid | |- ( -. E. x ph -> ( E! x ( ph \/ ps ) <-> E! x ps ) ) |