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

Metamath Proof Explorer

Theorem mof

Description: Version of df-mo with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by NM, 8-Mar-1995) Extract dfmo from this proof, and prove mof from it (as of 30-Sep-2022, directly from df-mo ). (Revised by Wolf Lammen, 28-May-2019) Avoid ax-13 . (Revised by Wolf Lammen, 16-Oct-2022)

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

Proof

Step Hyp Ref Expression
1 mof.1 
 |-  F/ y ph
2 df-mo 
 |-  ( E* x ph <-> E. z A. x ( ph -> x = z ) )
3 nfv 
 |-  F/ y x = z
4 1 3 nfim 
 |-  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 imbi2d 
 |-  ( 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 ) )