Theorem moexex 2273

Description: "At most one" double quantification. (Contributed by NM, 3-Dec-2001.)

Hypothesis

Ref	Expression
moexex.1	|- F/yph

Assertion

Ref	Expression
moexex	|- ((E*xph /\ A.xE*yps) -> E*yE.x(ph /\ ps))

Proof of Theorem moexex

Step	Hyp	Ref	Expression
1		nfmo1 2215	. . . . 5 |- F/xE*xph
2		nfa1 1788	. . . . . 6 |- F/xA.xE*yps
3		nfe1 1732	. . . . . . 7 |- F/xE.x(ph /\ ps)
4	3	nfmo 2221	. . . . . 6 |- F/xE*yE.x(ph /\ ps)
5	2, 4	nfim 1813	. . . . 5 |- F/x(A.xE*yps -> E*yE.x(ph /\ ps))
6	1, 5	nfim 1813	. . . 4 |- F/x(E*xph -> (A.xE*yps -> E*yE.x(ph /\ ps)))
7		moexex.1	. . . . . 6 |- F/yph
8	7	nfmo 2221	. . . . . 6 |- F/yE*xph
9		mopick 2266	. . . . . . . 8 |- ((E*xph /\ E.x(ph /\ ps)) -> (ph -> ps))
10	9	ex 423	. . . . . . 7 |- (E*xph -> (E.x(ph /\ ps) -> (ph -> ps)))
11	10	com3r 73	. . . . . 6 |- (ph -> (E*xph -> (E.x(ph /\ ps) -> ps)))
12	7, 8, 11	alrimd 1769	. . . . 5 |- (ph -> (E*xph -> A.y(E.x(ph /\ ps) -> ps)))
13		moim 2250	. . . . . 6 |- (A.y(E.x(ph /\ ps) -> ps) -> (E*yps -> E*yE.x(ph /\ ps)))
14	13	spsd 1755	. . . . 5 |- (A.y(E.x(ph /\ ps) -> ps) -> (A.xE*yps -> E*yE.x(ph /\ ps)))
15	12, 14	syl6 29	. . . 4 |- (ph -> (E*xph -> (A.xE*yps -> E*yE.x(ph /\ ps))))
16	6, 15	exlimi 1803	. . 3 |- (E.xph -> (E*xph -> (A.xE*yps -> E*yE.x(ph /\ ps))))
17	7	nfex 1843	. . . . . . . 8 |- F/yE.xph
18		exsimpl 1592	. . . . . . . 8 |- (E.x(ph /\ ps) -> E.xph)
19	17, 18	exlimi 1803	. . . . . . 7 |- (E.yE.x(ph /\ ps) -> E.xph)
20	19	con3i 127	. . . . . 6 |- (-. E.xph -> -. E.yE.x(ph /\ ps))
21		exmo 2249	. . . . . . 7 |- (E.yE.x(ph /\ ps) \/ E*yE.x(ph /\ ps))
22	21	ori 364	. . . . . 6 |- (-. E.yE.x(ph /\ ps) -> E*yE.x(ph /\ ps))
23	20, 22	syl 15	. . . . 5 |- (-. E.xph -> E*yE.x(ph /\ ps))
24	23	a1d 22	. . . 4 |- (-. E.xph -> (A.xE*yps -> E*yE.x(ph /\ ps)))
25	24	a1d 22	. . 3 |- (-. E.xph -> (E*xph -> (A.xE*yps -> E*yE.x(ph /\ ps))))
26	16, 25	pm2.61i 156	. 2 |- (E*xph -> (A.xE*yps -> E*yE.x(ph /\ ps)))
27	26	imp 418	1 |- ((E*xph /\ A.xE*yps) -> E*yE.x(ph /\ ps))

Syntax hints:  -. wn 3   -> wi 4   /\ wa 358  A.wal 1540  E.wex 1541   F/wnf 1544  E*wmo 2205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209

This theorem is referenced by:  moexexv  2274  2moswap  2279