Metamath Proof Explorer

Theorem wl-mo2df

Description: Version of mof with a context and a distinctor replacing a distinct variable condition. This version should be used only to eliminate disjoint variable conditions. (Contributed by Wolf Lammen, 11-Aug-2019)

Ref Expression
Hypotheses wl-mo2df.1 
|- F/ x ph
wl-mo2df.2 
|- F/ y ph
wl-mo2df.3 
|- ( ph -> -. A. x x = y )
wl-mo2df.4 
|- ( ph -> F/ y ps )
Assertion wl-mo2df 
|- ( ph -> ( E* x ps <-> E. y A. x ( ps -> x = y ) ) )

Proof

Step Hyp Ref Expression
1 wl-mo2df.1 
 |-  F/ x ph
2 wl-mo2df.2 
 |-  F/ y ph
3 wl-mo2df.3 
 |-  ( ph -> -. A. x x = y )
4 wl-mo2df.4 
 |-  ( ph -> F/ y ps )
5 df-mo 
 |-  ( E* x ps <-> E. u A. x ( ps -> x = u ) )
6 nfeqf1 
 |-  ( -. A. y y = x -> F/ y x = u )
7 6 naecoms 
 |-  ( -. A. x x = y -> F/ y x = u )
8 3 7 syl 
 |-  ( ph -> F/ y x = u )
9 4 8 nfimd 
 |-  ( ph -> F/ y ( ps -> x = u ) )
10 1 9 nfald 
 |-  ( ph -> F/ y A. x ( ps -> x = u ) )
11 nfnae 
 |-  F/ x -. A. x x = y
12 nfeqf2 
 |-  ( -. A. x x = y -> F/ x u = y )
13 11 12 nfan1 
 |-  F/ x ( -. A. x x = y /\ u = y )
14 equequ2 
 |-  ( u = y -> ( x = u <-> x = y ) )
15 14 imbi2d 
 |-  ( u = y -> ( ( ps -> x = u ) <-> ( ps -> x = y ) ) )
16 15 adantl 
 |-  ( ( -. A. x x = y /\ u = y ) -> ( ( ps -> x = u ) <-> ( ps -> x = y ) ) )
17 13 16 albid 
 |-  ( ( -. A. x x = y /\ u = y ) -> ( A. x ( ps -> x = u ) <-> A. x ( ps -> x = y ) ) )
18 3 17 sylan 
 |-  ( ( ph /\ u = y ) -> ( A. x ( ps -> x = u ) <-> A. x ( ps -> x = y ) ) )
19 18 ex 
 |-  ( ph -> ( u = y -> ( A. x ( ps -> x = u ) <-> A. x ( ps -> x = y ) ) ) )
20 2 10 19 cbvexd 
 |-  ( ph -> ( E. u A. x ( ps -> x = u ) <-> E. y A. x ( ps -> x = y ) ) )
21 5 20 syl5bb 
 |-  ( ph -> ( E* x ps <-> E. y A. x ( ps -> x = y ) ) )