Description: Version of eu3v where the disjoint variable condition is replaced with a nonfreeness hypothesis. This is a "backup" of a theorem that used to be in the main part with label "eu3" and was deprecated in favor of eu3v . (Contributed by NM, 8-Jul-1994) (Proof shortened by BJ, 31-May-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | bj-eu3f.1 | |- F/ y ph |
|
| Assertion | bj-eu3f | |- ( E! x ph <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-eu3f.1 | |- F/ y ph |
|
| 2 | df-eu | |- ( E! x ph <-> ( E. x ph /\ E* x ph ) ) |
|
| 3 | 1 | mof | |- ( E* x ph <-> E. y A. x ( ph -> x = y ) ) |
| 4 | 3 | anbi2i | |- ( ( E. x ph /\ E* x ph ) <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) ) |
| 5 | 2 4 | bitri | |- ( E! x ph <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) ) |