Description: Introduce a disjunct into a unique existential quantifier. For a version requiring disjoint variables, but fewer axioms, see euorv . (Contributed by NM, 21-Oct-2005)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | euor.nf | |- F/ x ph |
|
| Assertion | euor | |- ( ( -. ph /\ E! x ps ) -> E! x ( ph \/ ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | euor.nf | |- F/ x ph |
|
| 2 | 1 | nfn | |- F/ x -. ph |
| 3 | biorf | |- ( -. ph -> ( ps <-> ( ph \/ ps ) ) ) |
|
| 4 | 2 3 | eubid | |- ( -. ph -> ( E! x ps <-> E! x ( ph \/ ps ) ) ) |
| 5 | 4 | biimpa | |- ( ( -. ph /\ E! x ps ) -> E! x ( ph \/ ps ) ) |