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 ) )