Metamath Proof Explorer

Theorem mosubott

Description: "At most one" remains true inside ordered triple quantification, analogous to mosubopt . (Contributed by BTernaryTau, 8-Sep-2026)

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

Proof

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