Description: Introduce a disjunct into a unique existential quantifier. Version of euor requiring disjoint variables, but fewer axioms. (Contributed by NM, 23-Mar-1995) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | euorv | |- ( ( -. ph /\ E! x ps ) -> E! x ( ph \/ ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | biorf | |- ( -. ph -> ( ps <-> ( ph \/ ps ) ) ) |
|
| 2 | 1 | eubidv | |- ( -. ph -> ( E! x ps <-> E! x ( ph \/ ps ) ) ) |
| 3 | 2 | biimpa | |- ( ( -. ph /\ E! x ps ) -> E! x ( ph \/ ps ) ) |