Metamath Proof Explorer

Theorem wl-mo2t

Description: Closed form of mof . (Contributed by Wolf Lammen, 18-Aug-2019)

Ref Expression
Assertion wl-mo2t 
|- ( A. x F/ y ph -> ( E* x ph <-> E. y A. x ( ph -> x = y ) ) )

Proof

Step Hyp Ref Expression
1 df-mo 
 |-  ( E* x ph <-> E. u A. x ( ph -> x = u ) )
2 nfnf1 
 |-  F/ y F/ y ph
3 2 nfal 
 |-  F/ y A. x F/ y ph
4 nfa1 
 |-  F/ x A. x F/ y ph
5 sp 
 |-  ( A. x F/ y ph -> F/ y ph )
6 nfvd 
 |-  ( A. x F/ y ph -> F/ y x = u )
7 5 6 nfimd 
 |-  ( A. x F/ y ph -> F/ y ( ph -> x = u ) )
8 4 7 nfald 
 |-  ( A. x F/ y ph -> F/ y A. x ( ph -> x = u ) )
9 equequ2 
 |-  ( u = y -> ( x = u <-> x = y ) )
10 9 imbi2d 
 |-  ( u = y -> ( ( ph -> x = u ) <-> ( ph -> x = y ) ) )
11 10 albidv 
 |-  ( u = y -> ( A. x ( ph -> x = u ) <-> A. x ( ph -> x = y ) ) )
12 11 a1i 
 |-  ( A. x F/ y ph -> ( u = y -> ( A. x ( ph -> x = u ) <-> A. x ( ph -> x = y ) ) ) )
13 3 8 12 cbvexdw 
 |-  ( A. x F/ y ph -> ( E. u A. x ( ph -> x = u ) <-> E. y A. x ( ph -> x = y ) ) )
14 1 13 syl5bb 
 |-  ( A. x F/ y ph -> ( E* x ph <-> E. y A. x ( ph -> x = y ) ) )