Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim requiring disjoint variables, but fewer axioms. (Contributed by NM, 23-Mar-1995) Reduce axiom usage . (Revised by Wolf Lammen, 8-Feb-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | moanimv | |- ( E* x ( ph /\ ps ) <-> ( ph -> E* x ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ibar | |- ( ph -> ( ps <-> ( ph /\ ps ) ) ) |
|
| 2 | 1 | mobidv | |- ( ph -> ( E* x ps <-> E* x ( ph /\ ps ) ) ) |
| 3 | simpl | |- ( ( ph /\ ps ) -> ph ) |
|
| 4 | 3 | exlimiv | |- ( E. x ( ph /\ ps ) -> ph ) |
| 5 | 2 4 | moanimlem | |- ( E* x ( ph /\ ps ) <-> ( ph -> E* x ps ) ) |