Metamath Proof Explorer

Theorem wl-mo2tf

Description: Closed form of mof with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 20-Sep-2020)

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

Proof

Step Hyp Ref Expression
1 nfnae 
 |-  F/ x -. A. x x = y
2 nfa1 
 |-  F/ x A. x F/ y ph
3 1 2 nfan 
 |-  F/ x ( -. A. x x = y /\ A. x F/ y ph )
4 nfnae 
 |-  F/ y -. A. x x = y
5 nfnf1 
 |-  F/ y F/ y ph
6 5 nfal 
 |-  F/ y A. x F/ y ph
7 4 6 nfan 
 |-  F/ y ( -. A. x x = y /\ A. x F/ y ph )
8 simpl 
 |-  ( ( -. A. x x = y /\ A. x F/ y ph ) -> -. A. x x = y )
9 sp 
 |-  ( A. x F/ y ph -> F/ y ph )
10 9 adantl 
 |-  ( ( -. A. x x = y /\ A. x F/ y ph ) -> F/ y ph )
11 3 7 8 10 wl-mo2df 
 |-  ( ( -. A. x x = y /\ A. x F/ y ph ) -> ( E* x ph <-> E. y A. x ( ph -> x = y ) ) )