Metamath Proof Explorer


Theorem 2mos

Description: Double "there exists at most one", using implicit substitution. (Contributed by NM, 10-Feb-2005) (Proof shortened by Wolf Lammen, 21-May-2025)

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 1 2sbievw
 |-  ( [ z / x ] [ w / y ] ph <-> ps )
4 3 anbi2i
 |-  ( ( ph /\ [ z / x ] [ w / y ] ph ) <-> ( ph /\ ps ) )
5 4 imbi1i
 |-  ( ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) <-> ( ( ph /\ ps ) -> ( x = z /\ y = w ) ) )
6 5 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 ) ) )
7 6 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 ) ) )
8 2 7 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 ) ) )