Theorem eu6lem

Description: Lemma of eu6im . A dissection of an idiom characterizing existential uniqueness. (Contributed by NM, 12-Aug-1993) This used to be the definition of the unique existential quantifier, while df-eu was then proved as dfeu . (Revised by BJ, 30-Sep-2022) (Proof shortened by Wolf Lammen, 3-Jan-2023) Extract common proof lines. (Revised by Wolf Lammen, 3-Mar-2023)

	Ref	Expression
Assertion	eu6lem	|- ( E. y A. x ( ph <-> x = y ) <-> ( E. y A. x ( x = y -> ph ) /\ E. z A. x ( ph -> x = z ) ) )

Proof

Step	Hyp	Ref	Expression
1		19.42v	|- ( E. z ( A. x ( ph <-> x = y ) /\ y = z ) <-> ( A. x ( ph <-> x = y ) /\ E. z y = z ) )
2		alsyl	|- ( ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) -> A. x ( x = y -> x = z ) )
3		equvelv	|- ( A. x ( x = y -> x = z ) <-> y = z )
4	2 3	sylib	|- ( ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) -> y = z )
5	4	pm4.71i	|- ( ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) <-> ( ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) /\ y = z ) )
6		albiim	|- ( A. x ( ph <-> x = y ) <-> ( A. x ( ph -> x = y ) /\ A. x ( x = y -> ph ) ) )
7	6	biancomi	|- ( A. x ( ph <-> x = y ) <-> ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = y ) ) )
8		equequ2	|- ( y = z -> ( x = y <-> x = z ) )
9	8	imbi2d	|- ( y = z -> ( ( ph -> x = y ) <-> ( ph -> x = z ) ) )
10	9	albidv	|- ( y = z -> ( A. x ( ph -> x = y ) <-> A. x ( ph -> x = z ) ) )
11	10	anbi2d	|- ( y = z -> ( ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = y ) ) <-> ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) ) )
12	7 11	syl5bb	|- ( y = z -> ( A. x ( ph <-> x = y ) <-> ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) ) )
13	12	pm5.32ri	|- ( ( A. x ( ph <-> x = y ) /\ y = z ) <-> ( ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) /\ y = z ) )
14	5 13	bitr4i	|- ( ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) <-> ( A. x ( ph <-> x = y ) /\ y = z ) )
15	14	exbii	|- ( E. z ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) <-> E. z ( A. x ( ph <-> x = y ) /\ y = z ) )
16		ax6evr	|- E. z y = z
17	16	biantru	|- ( A. x ( ph <-> x = y ) <-> ( A. x ( ph <-> x = y ) /\ E. z y = z ) )
18	1 15 17	3bitr4ri	|- ( A. x ( ph <-> x = y ) <-> E. z ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) )
19	18	exbii	|- ( E. y A. x ( ph <-> x = y ) <-> E. y E. z ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) )
20		exdistrv	|- ( E. y E. z ( A. x ( x = y -> ph ) /\ A. x ( ph -> x = z ) ) <-> ( E. y A. x ( x = y -> ph ) /\ E. z A. x ( ph -> x = z ) ) )
21	19 20	bitri	|- ( E. y A. x ( ph <-> x = y ) <-> ( E. y A. x ( x = y -> ph ) /\ E. z A. x ( ph -> x = z ) ) )