Metamath Proof Explorer

Theorem wl-eudf

Description: Version of eu6 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, 23-Sep-2020)

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

Proof

Step Hyp Ref Expression
1 wl-eudf.1 
 |-  F/ x ph
2 wl-eudf.2 
 |-  F/ y ph
3 wl-eudf.3 
 |-  ( ph -> -. A. x x = y )
4 wl-eudf.4 
 |-  ( ph -> F/ y ps )
5 eu6 
 |-  ( 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 nfbid 
 |-  ( 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 bibi2d 
 |-  ( 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 ) ) )