Theorem 2eu6 2558

Description: Two equivalent expressions for double existential uniqueness. (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 2-Oct-2019.)

Assertion

Ref	Expression
2eu6	|- ( ( E! x E. y ph /\ E! y E. x ph ) <-> E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) )

Distinct variable groups:   x, y, z, w   ph, z, w

Allowed substitution hints:   ph( x, y)

Proof of Theorem 2eu6

Step	Hyp	Ref	Expression
1		2eu4 2556	. 2 |- ( ( E! x E. y ph /\ E! y E. x ph ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
2		nfia1 2030	. . . . . 6 |- F/ x ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> A. x A. y ( ph <-> ( x = z /\ y = w ) ) )
3		nfa1 2028	. . . . . . . . . . . . 13 |- F/ y A. y ( ph -> ( x = z /\ y = w ) )
4		nfv 1843	. . . . . . . . . . . . 13 |- F/ y x = z
5		simpl 473	. . . . . . . . . . . . . . 15 |- ( ( x = z /\ y = w ) -> x = z )
6	5	imim2i 16	. . . . . . . . . . . . . 14 |- ( ( ph -> ( x = z /\ y = w ) ) -> ( ph -> x = z ) )
7	6	sps 2055	. . . . . . . . . . . . 13 |- ( A. y ( ph -> ( x = z /\ y = w ) ) -> ( ph -> x = z ) )
8	3, 4, 7	exlimd 2087	. . . . . . . . . . . 12 |- ( A. y ( ph -> ( x = z /\ y = w ) ) -> ( E. y ph -> x = z ) )
9		ax12v 2048	. . . . . . . . . . . 12 |- ( x = z -> ( E. y ph -> A. x ( x = z -> E. y ph ) ) )
10	8, 9	syli 39	. . . . . . . . . . 11 |- ( A. y ( ph -> ( x = z /\ y = w ) ) -> ( E. y ph -> A. x ( x = z -> E. y ph ) ) )
11	10	com12 32	. . . . . . . . . 10 |- ( E. y ph -> ( A. y ( ph -> ( x = z /\ y = w ) ) -> A. x ( x = z -> E. y ph ) ) )
12	11	spsd 2057	. . . . . . . . 9 |- ( E. y ph -> ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> A. x ( x = z -> E. y ph ) ) )
13		nfs1v 2437	. . . . . . . . . . . . 13 |- F/ y [ w / y ] ph
14		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( x = z /\ y = w ) -> y = w )
15	14	imim2i 16	. . . . . . . . . . . . . . 15 |- ( ( ph -> ( x = z /\ y = w ) ) -> ( ph -> y = w ) )
16		sbequ1 2110	. . . . . . . . . . . . . . 15 |- ( y = w -> ( ph -> [ w / y ] ph ) )
17	15, 16	syli 39	. . . . . . . . . . . . . 14 |- ( ( ph -> ( x = z /\ y = w ) ) -> ( ph -> [ w / y ] ph ) )
18	17	sps 2055	. . . . . . . . . . . . 13 |- ( A. y ( ph -> ( x = z /\ y = w ) ) -> ( ph -> [ w / y ] ph ) )
19	3, 13, 18	exlimd 2087	. . . . . . . . . . . 12 |- ( A. y ( ph -> ( x = z /\ y = w ) ) -> ( E. y ph -> [ w / y ] ph ) )
20	19	imim2d 57	. . . . . . . . . . 11 |- ( A. y ( ph -> ( x = z /\ y = w ) ) -> ( ( x = z -> E. y ph ) -> ( x = z -> [ w / y ] ph ) ) )
21	20	al2imi 1743	. . . . . . . . . 10 |- ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> ( A. x ( x = z -> E. y ph ) -> A. x ( x = z -> [ w / y ] ph ) ) )
22		sb6 2429	. . . . . . . . . . 11 |- ( [ z / x ] [ w / y ] ph <-> A. x ( x = z -> [ w / y ] ph ) )
23		2sb6 2444	. . . . . . . . . . 11 |- ( [ z / x ] [ w / y ] ph <-> A. x A. y ( ( x = z /\ y = w ) -> ph ) )
24	22, 23	bitr3i 266	. . . . . . . . . 10 |- ( A. x ( x = z -> [ w / y ] ph ) <-> A. x A. y ( ( x = z /\ y = w ) -> ph ) )
25	21, 24	syl6ib 241	. . . . . . . . 9 |- ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> ( A. x ( x = z -> E. y ph ) -> A. x A. y ( ( x = z /\ y = w ) -> ph ) ) )
26	12, 25	sylcom 30	. . . . . . . 8 |- ( E. y ph -> ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> A. x A. y ( ( x = z /\ y = w ) -> ph ) ) )
27	26	ancld 576	. . . . . . 7 |- ( E. y ph -> ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> ( A. x A. y ( ph -> ( x = z /\ y = w ) ) /\ A. x A. y ( ( x = z /\ y = w ) -> ph ) ) ) )
28		2albiim 1817	. . . . . . 7 |- ( A. x A. y ( ph <-> ( x = z /\ y = w ) ) <-> ( A. x A. y ( ph -> ( x = z /\ y = w ) ) /\ A. x A. y ( ( x = z /\ y = w ) -> ph ) ) )
29	27, 28	syl6ibr 242	. . . . . 6 |- ( E. y ph -> ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> A. x A. y ( ph <-> ( x = z /\ y = w ) ) ) )
30	2, 29	exlimi 2086	. . . . 5 |- ( E. x E. y ph -> ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> A. x A. y ( ph <-> ( x = z /\ y = w ) ) ) )
31	30	2eximdv 1848	. . . 4 |- ( E. x E. y ph -> ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) -> E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) ) )
32	31	imp 445	. . 3 |- ( ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) -> E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) )
33		biimpr 210	. . . . . . 7 |- ( ( ph <-> ( x = z /\ y = w ) ) -> ( ( x = z /\ y = w ) -> ph ) )
34	33	2alimi 1740	. . . . . 6 |- ( A. x A. y ( ph <-> ( x = z /\ y = w ) ) -> A. x A. y ( ( x = z /\ y = w ) -> ph ) )
35	34	2eximi 1763	. . . . 5 |- ( E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) -> E. z E. w A. x A. y ( ( x = z /\ y = w ) -> ph ) )
36		2exsb 2469	. . . . 5 |- ( E. x E. y ph <-> E. z E. w A. x A. y ( ( x = z /\ y = w ) -> ph ) )
37	35, 36	sylibr 224	. . . 4 |- ( E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) -> E. x E. y ph )
38		biimp 205	. . . . . 6 |- ( ( ph <-> ( x = z /\ y = w ) ) -> ( ph -> ( x = z /\ y = w ) ) )
39	38	2alimi 1740	. . . . 5 |- ( A. x A. y ( ph <-> ( x = z /\ y = w ) ) -> A. x A. y ( ph -> ( x = z /\ y = w ) ) )
40	39	2eximi 1763	. . . 4 |- ( E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
41	37, 40	jca 554	. . 3 |- ( E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) -> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
42	32, 41	impbii 199	. 2 |- ( ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) <-> E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) )
43	1, 42	bitri 264	1 |- ( ( E! x E. y ph /\ E! y E. x ph ) <-> E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   E.wex 1704   [wsb 1880   E!weu 2470

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)