Theorem 2eu1 1067

Description: Double existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one.

Assertion

Ref	Expression
2eu1	|- (A.xE*yph -> (E!xE!yph <-> (E!xE.yph /\ E!yE.xph)))

Proof of Theorem 2eu1

Step	Hyp	Ref	Expression
1		2eu2ex 1063	. . . . . . 7 |- (E!xE!yph -> E.xE.yph)
2		excom 728	. . . . . . . 8 |- (E.xE.yph <-> E.yE.xph)
3	1, 2	sylib 173	. . . . . . 7 |- (E!xE!yph -> E.yE.xph)
4	1, 3	jca 236	. . . . . 6 |- (E!xE!yph -> (E.xE.yph /\ E.yE.xph))
5	4	a1d 14	. . . . 5 |- (E!xE!yph -> (A.xE*yph -> (E.xE.yph /\ E.yE.xph)))
6		eu5 1035	. . . . . . . 8 |- (E!xE!yph <-> (E.xE!yph /\ E*xE!yph))
7		eu5 1035	. . . . . . . . . 10 |- (E!yph <-> (E.yph /\ E*yph))
8	7	biex 733	. . . . . . . . 9 |- (E.xE!yph <-> E.x(E.yph /\ E*yph))
9	7	bimo 1031	. . . . . . . . 9 |- (E*xE!yph <-> E*x(E.yph /\ E*yph))
10	8, 9	anbi12i 369	. . . . . . . 8 |- ((E.xE!yph /\ E*xE!yph) <-> (E.x(E.yph /\ E*yph) /\ E*x(E.yph /\ E*yph)))
11	6, 10	bitr 151	. . . . . . 7 |- (E!xE!yph <-> (E.x(E.yph /\ E*yph) /\ E*x(E.yph /\ E*yph)))
12	11	pm3.27bd 263	. . . . . 6 |- (E!xE!yph -> E*x(E.yph /\ E*yph))
13		immo 1043	. . . . . . . . . 10 |- (A.x((A.xE*yph /\ E.yph) -> (E.yph /\ E*yph)) -> (E*x(E.yph /\ E*yph) -> E*x(A.xE*yph /\ E.yph)))
14		ax-4 673	. . . . . . . . . . . 12 |- (A.xE*yph -> E*yph)
15	14	anim2i 270	. . . . . . . . . . 11 |- ((E.yph /\ A.xE*yph) -> (E.yph /\ E*yph))
16	15	ancoms 334	. . . . . . . . . 10 |- ((A.xE*yph /\ E.yph) -> (E.yph /\ E*yph))
17	13, 16	mpg 684	. . . . . . . . 9 |- (E*x(E.yph /\ E*yph) -> E*x(A.xE*yph /\ E.yph))
18		hba1 698	. . . . . . . . . 10 |- (A.xE*yph -> A.xA.xE*yph)
19	18	moanim 1051	. . . . . . . . 9 |- (E*x(A.xE*yph /\ E.yph) <-> (A.xE*yph -> E*xE.yph))
20	17, 19	sylib 173	. . . . . . . 8 |- (E*x(E.yph /\ E*yph) -> (A.xE*yph -> E*xE.yph))
21	20	ancrd 247	. . . . . . 7 |- (E*x(E.yph /\ E*yph) -> (A.xE*yph -> (E*xE.yph /\ A.xE*yph)))
22		2moswap 1064	. . . . . . . . 9 |- (A.xE*yph -> (E*xE.yph -> E*yE.xph))
23	22	com12 13	. . . . . . . 8 |- (E*xE.yph -> (A.xE*yph -> E*yE.xph))
24	23	imdistani 340	. . . . . . 7 |- ((E*xE.yph /\ A.xE*yph) -> (E*xE.yph /\ E*yE.xph))
25	21, 24	syl6 23	. . . . . 6 |- (E*x(E.yph /\ E*yph) -> (A.xE*yph -> (E*xE.yph /\ E*yE.xph)))
26	12, 25	syl 12	. . . . 5 |- (E!xE!yph -> (A.xE*yph -> (E*xE.yph /\ E*yE.xph)))
27	5, 26	jcad 455	. . . 4 |- (E!xE!yph -> (A.xE*yph -> ((E.xE.yph /\ E.yE.xph) /\ (E*xE.yph /\ E*yE.xph))))
28		eu5 1035	. . . . . 6 |- (E!xE.yph <-> (E.xE.yph /\ E*xE.yph))
29		eu5 1035	. . . . . 6 |- (E!yE.xph <-> (E.yE.xph /\ E*yE.xph))
30	28, 29	anbi12i 369	. . . . 5 |- ((E!xE.yph /\ E!yE.xph) <-> ((E.xE.yph /\ E*xE.yph) /\ (E.yE.xph /\ E*yE.xph)))
31		an4 388	. . . . 5 |- (((E.xE.yph /\ E*xE.yph) /\ (E.yE.xph /\ E*yE.xph)) <-> ((E.xE.yph /\ E.yE.xph) /\ (E*xE.yph /\ E*yE.xph)))
32	30, 31	bitr 151	. . . 4 |- ((E!xE.yph /\ E!yE.xph) <-> ((E.xE.yph /\ E.yE.xph) /\ (E*xE.yph /\ E*yE.xph)))
33	27, 32	syl6ibr 186	. . 3 |- (E!xE!yph -> (A.xE*yph -> (E!xE.yph /\ E!yE.xph)))
34	33	com12 13	. 2 |- (A.xE*yph -> (E!xE!yph -> (E!xE.yph /\ E!yE.xph)))
35		2exeu 1066	. . 3 |- ((E!xE.yph /\ E!yE.xph) -> E!xE!yph)
36	35	a1i 7	. 2 |- (A.xE*yph -> ((E!xE.yph /\ E!yE.xph) -> E!xE!yph))
37	34, 36	impbid 397	1 |- (A.xE*yph -> (E!xE!yph <-> (E!xE.yph /\ E!yE.xph)))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196  A.wal 672  E.wex 678  E!weu 1007  E*wmo 1008

This theorem is referenced by:  2eu2 1068  2eu3 1069  2eu5 1071

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010

metamath.org