Metamath Proof Explorer


Theorem mosubopt

Description: "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007)

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

Proof

Step Hyp Ref Expression
1 nfa1
 |-  F/ y A. y A. z E* x ph
2 nfe1
 |-  F/ y E. y E. z ( A = <. y , z >. /\ ph )
3 2 nfmov
 |-  F/ y E* x E. y E. z ( A = <. y , z >. /\ ph )
4 nfa1
 |-  F/ z A. z E* x ph
5 nfe1
 |-  F/ z E. z ( A = <. y , z >. /\ ph )
6 5 nfex
 |-  F/ z E. y E. z ( A = <. y , z >. /\ ph )
7 6 nfmov
 |-  F/ z E* x E. y E. z ( A = <. y , z >. /\ ph )
8 copsexgw
 |-  ( A = <. y , z >. -> ( ph <-> E. y E. z ( A = <. y , z >. /\ ph ) ) )
9 8 mobidv
 |-  ( A = <. y , z >. -> ( E* x ph <-> E* x E. y E. z ( A = <. y , z >. /\ ph ) ) )
10 9 biimpcd
 |-  ( E* x ph -> ( A = <. y , z >. -> E* x E. y E. z ( A = <. y , z >. /\ ph ) ) )
11 10 sps
 |-  ( A. z E* x ph -> ( A = <. y , z >. -> E* x E. y E. z ( A = <. y , z >. /\ ph ) ) )
12 4 7 11 exlimd
 |-  ( A. z E* x ph -> ( E. z A = <. y , z >. -> E* x E. y E. z ( A = <. y , z >. /\ ph ) ) )
13 12 sps
 |-  ( A. y A. z E* x ph -> ( E. z A = <. y , z >. -> E* x E. y E. z ( A = <. y , z >. /\ ph ) ) )
14 1 3 13 exlimd
 |-  ( A. y A. z E* x ph -> ( E. y E. z A = <. y , z >. -> E* x E. y E. z ( A = <. y , z >. /\ ph ) ) )
15 simpl
 |-  ( ( A = <. y , z >. /\ ph ) -> A = <. y , z >. )
16 15 2eximi
 |-  ( E. y E. z ( A = <. y , z >. /\ ph ) -> E. y E. z A = <. y , z >. )
17 16 exlimiv
 |-  ( E. x E. y E. z ( A = <. y , z >. /\ ph ) -> E. y E. z A = <. y , z >. )
18 nexmo
 |-  ( -. E. x E. y E. z ( A = <. y , z >. /\ ph ) -> E* x E. y E. z ( A = <. y , z >. /\ ph ) )
19 17 18 nsyl5
 |-  ( -. E. y E. z A = <. y , z >. -> E* x E. y E. z ( A = <. y , z >. /\ ph ) )
20 14 19 pm2.61d1
 |-  ( A. y A. z E* x ph -> E* x E. y E. z ( A = <. y , z >. /\ ph ) )