Metamath Proof Explorer


Theorem bj-eu3f

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

Proof

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