Theorem wl-mo3t 33358

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

Assertion

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

Distinct variable group:   x, y

Allowed substitution hints:   ph( x, y)

Proof of Theorem wl-mo3t

Dummy variable u is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfa1 2028	. . 3 |- F/ x A. x F/ y ph
2		nfmo1 2481	. . 3 |- F/ x E* x ph
3		nfnf1 2031	. . . . . . 7 |- F/ y F/ y ph
4	3	nfal 2153	. . . . . 6 |- F/ y A. x F/ y ph
5		sp 2053	. . . . . . 7 |- ( A. x F/ y ph -> F/ y ph )
6	1, 5	nfmod 2485	. . . . . 6 |- ( A. x F/ y ph -> F/ y E* x ph )
7	4, 6	nfan1 2068	. . . . 5 |- F/ y ( A. x F/ y ph /\ E* x ph )
8		mo2v 2477	. . . . . . 7 |- ( E* x ph <-> E. u A. x ( ph -> x = u ) )
9		sp 2053	. . . . . . . . . 10 |- ( A. x ( ph -> x = u ) -> ( ph -> x = u ) )
10		spsbim 2394	. . . . . . . . . . 11 |- ( A. x ( ph -> x = u ) -> ( [ y / x ] ph -> [ y / x ] x = u ) )
11		equsb3 2432	. . . . . . . . . . 11 |- ( [ y / x ] x = u <-> y = u )
12	10, 11	syl6ib 241	. . . . . . . . . 10 |- ( A. x ( ph -> x = u ) -> ( [ y / x ] ph -> y = u ) )
13	9, 12	anim12d 586	. . . . . . . . 9 |- ( A. x ( ph -> x = u ) -> ( ( ph /\ [ y / x ] ph ) -> ( x = u /\ y = u ) ) )
14		equtr2 1954	. . . . . . . . 9 |- ( ( x = u /\ y = u ) -> x = y )
15	13, 14	syl6 35	. . . . . . . 8 |- ( A. x ( ph -> x = u ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) )
16	15	exlimiv 1858	. . . . . . 7 |- ( E. u A. x ( ph -> x = u ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) )
17	8, 16	sylbi 207	. . . . . 6 |- ( E* x ph -> ( ( ph /\ [ y / x ] ph ) -> x = y ) )
18	17	adantl 482	. . . . 5 |- ( ( A. x F/ y ph /\ E* x ph ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) )
19	7, 18	alrimi 2082	. . . 4 |- ( ( A. x F/ y ph /\ E* x ph ) -> A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
20	19	ex 450	. . 3 |- ( A. x F/ y ph -> ( E* x ph -> A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
21	1, 2, 20	alrimd 2084	. 2 |- ( A. x F/ y ph -> ( E* x ph -> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
22		nfa1 2028	. . . . . 6 |- F/ x A. x ( ( ph /\ [ y / x ] ph ) -> x = y )
23		nfs1v 2437	. . . . . 6 |- F/ x [ y / x ] ph
24		pm3.3 460	. . . . . . . 8 |- ( ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( ph -> ( [ y / x ] ph -> x = y ) ) )
25	24	com23 86	. . . . . . 7 |- ( ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( [ y / x ] ph -> ( ph -> x = y ) ) )
26	25	sps 2055	. . . . . 6 |- ( A. x ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( [ y / x ] ph -> ( ph -> x = y ) ) )
27	22, 23, 26	alrimd 2084	. . . . 5 |- ( A. x ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( [ y / x ] ph -> A. x ( ph -> x = y ) ) )
28	27	aleximi 1759	. . . 4 |- ( A. y A. x ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( E. y [ y / x ] ph -> E. y A. x ( ph -> x = y ) ) )
29	28	alcoms 2035	. . 3 |- ( A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( E. y [ y / x ] ph -> E. y A. x ( ph -> x = y ) ) )
30		moabs 2501	. . . 4 |- ( E* x ph <-> ( E. x ph -> E* x ph ) )
31		wl-sb8et 33334	. . . . 5 |- ( A. x F/ y ph -> ( E. x ph <-> E. y [ y / x ] ph ) )
32		wl-mo2t 33357	. . . . 5 |- ( A. x F/ y ph -> ( E* x ph <-> E. y A. x ( ph -> x = y ) ) )
33	31, 32	imbi12d 334	. . . 4 |- ( A. x F/ y ph -> ( ( E. x ph -> E* x ph ) <-> ( E. y [ y / x ] ph -> E. y A. x ( ph -> x = y ) ) ) )
34	30, 33	syl5bb 272	. . 3 |- ( A. x F/ y ph -> ( E* x ph <-> ( E. y [ y / x ] ph -> E. y A. x ( ph -> x = y ) ) ) )
35	29, 34	syl5ibr 236	. 2 |- ( A. x F/ y ph -> ( A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) -> E* x ph ) )
36	21, 35	impbid 202	1 |- ( A. x F/ y ph -> ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   E.wex 1704   F/wnf 1708   [wsb 1880   E*wmo 2471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475

This theorem is referenced by: (None)