Theorem 2mos

Description: Double "there exists at most one", using implicit substitution. (Contributed by NM, 10-Feb-2005)

	Ref	Expression
Hypothesis	2mos.1	|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )
Assertion	2mos	|- ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) <-> A. x A. y A. z A. w ( ( ph /\ ps ) -> ( x = z /\ y = w ) ) )

Proof

Step	Hyp	Ref	Expression
1		2mos.1	|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )
2		2mo	|- ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) <-> A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )
3		nfv	|- F/ y x = z
4	3	sbrim	|- ( [ w / y ] ( x = z -> ph ) <-> ( x = z -> [ w / y ] ph ) )
5	1	expcom	|- ( y = w -> ( x = z -> ( ph <-> ps ) ) )
6	5	pm5.74d	|- ( y = w -> ( ( x = z -> ph ) <-> ( x = z -> ps ) ) )
7	6	sbievw	|- ( [ w / y ] ( x = z -> ph ) <-> ( x = z -> ps ) )
8	4 7	bitr3i	|- ( ( x = z -> [ w / y ] ph ) <-> ( x = z -> ps ) )
9	8	pm5.74ri	|- ( x = z -> ( [ w / y ] ph <-> ps ) )
10	9	sbievw	|- ( [ z / x ] [ w / y ] ph <-> ps )
11	10	anbi2i	|- ( ( ph /\ [ z / x ] [ w / y ] ph ) <-> ( ph /\ ps ) )
12	11	imbi1i	|- ( ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) <-> ( ( ph /\ ps ) -> ( x = z /\ y = w ) ) )
13	12	2albii	|- ( A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) <-> A. z A. w ( ( ph /\ ps ) -> ( x = z /\ y = w ) ) )
14	13	2albii	|- ( A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) <-> A. x A. y A. z A. w ( ( ph /\ ps ) -> ( x = z /\ y = w ) ) )
15	2 14	bitri	|- ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) <-> A. x A. y A. z A. w ( ( ph /\ ps ) -> ( x = z /\ y = w ) ) )