Description: Rederive df-eu from the old definition eu6 . (Contributed by NM, 23-Mar-1995) (Proof shortened by Wolf Lammen, 25-May-2019) (Proof shortened by BJ, 7-Oct-2022) (Proof modification is discouraged.) Use df-eu instead. (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dfeu | |- ( E! x ph <-> ( E. x ph /\ E* x ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | abai | |- ( ( E. x ph /\ E! x ph ) <-> ( E. x ph /\ ( E. x ph -> E! x ph ) ) ) |
|
| 2 | euex | |- ( E! x ph -> E. x ph ) |
|
| 3 | 2 | pm4.71ri | |- ( E! x ph <-> ( E. x ph /\ E! x ph ) ) |
| 4 | moeu | |- ( E* x ph <-> ( E. x ph -> E! x ph ) ) |
|
| 5 | 4 | anbi2i | |- ( ( E. x ph /\ E* x ph ) <-> ( E. x ph /\ ( E. x ph -> E! x ph ) ) ) |
| 6 | 1 3 5 | 3bitr4i | |- ( E! x ph <-> ( E. x ph /\ E* x ph ) ) |