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 ) ) ) |