Theorem eujust

Description: Soundness justification theorem for eu6 when this was the definition of the unique existential quantifier (note that y and z need not be disjoint, although the weaker theorem with that disjoint variable condition added would be enough to justify the soundness of the definition). See eujustALT for a proof that provides an example of how it can be achieved through the use of dvelim . (Contributed by NM, 11-Mar-2010) (Proof shortened by Andrew Salmon, 9-Jul-2011)

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

Proof

Step	Hyp	Ref	Expression
1		equequ2	|- ( y = w -> ( x = y <-> x = w ) )
2	1	bibi2d	|- ( y = w -> ( ( ph <-> x = y ) <-> ( ph <-> x = w ) ) )
3	2	albidv	|- ( y = w -> ( A. x ( ph <-> x = y ) <-> A. x ( ph <-> x = w ) ) )
4	3	cbvexvw	|- ( E. y A. x ( ph <-> x = y ) <-> E. w A. x ( ph <-> x = w ) )
5		equequ2	|- ( w = z -> ( x = w <-> x = z ) )
6	5	bibi2d	|- ( w = z -> ( ( ph <-> x = w ) <-> ( ph <-> x = z ) ) )
7	6	albidv	|- ( w = z -> ( A. x ( ph <-> x = w ) <-> A. x ( ph <-> x = z ) ) )
8	7	cbvexvw	|- ( E. w A. x ( ph <-> x = w ) <-> E. z A. x ( ph <-> x = z ) )
9	4 8	bitri	|- ( E. y A. x ( ph <-> x = y ) <-> E. z A. x ( ph <-> x = z ) )