This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem euf

Description: Version of eu6 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by NM, 12-Aug-1993) (Proof shortened by Wolf Lammen, 30-Oct-2018) Avoid ax-13 . (Revised by Wolf Lammen, 16-Oct-2022)

Ref Expression
Hypothesis euf.1 
|- F/ y ph
Assertion euf 
|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )

Proof

Step Hyp Ref Expression
1 euf.1 
 |-  F/ y ph
2 eu6 
 |-  ( E! x ph <-> E. z A. x ( ph <-> x = z ) )
3 nfv 
 |-  F/ y x = z
4 1 3 nfbi 
 |-  F/ y ( ph <-> x = z )
5 4 nfal 
 |-  F/ y A. x ( ph <-> x = z )
6 nfv 
 |-  F/ z A. x ( ph <-> x = y )
7 equequ2 
 |-  ( z = y -> ( x = z <-> x = y ) )
8 7 bibi2d 
 |-  ( z = y -> ( ( ph <-> x = z ) <-> ( ph <-> x = y ) ) )
9 8 albidv 
 |-  ( z = y -> ( A. x ( ph <-> x = z ) <-> A. x ( ph <-> x = y ) ) )
10 5 6 9 cbvexv1 
 |-  ( E. z A. x ( ph <-> x = z ) <-> E. y A. x ( ph <-> x = y ) )
11 2 10 bitri 
 |-  ( E! x ph <-> E. y A. x ( ph <-> x = y ) )