Theorem mo4

Description: At-most-one quantifier expressed using implicit substitution. This theorem is also a direct consequence of mo4f , but this proof is based on fewer axioms.

By the way, swapping x , y and ph , ps leads to an expression for E* y ps , which is equivalent to E* x ph (is a proof line), so the right hand side is a rare instance of an expression where swapping the quantifiers can be done without ax-11 . (Contributed by NM, 26-Jul-1995) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2023)

	Ref	Expression
Hypothesis	mo4.1	|- ( x = y -> ( ph <-> ps ) )
Assertion	mo4	|- ( E* x ph <-> A. x A. y ( ( ph /\ ps ) -> x = y ) )

Proof

Step	Hyp	Ref	Expression
1		mo4.1	|- ( x = y -> ( ph <-> ps ) )
2		df-mo	|- ( E* x ph <-> E. z A. x ( ph -> x = z ) )
3		equequ1	|- ( x = y -> ( x = z <-> y = z ) )
4	1 3	imbi12d	|- ( x = y -> ( ( ph -> x = z ) <-> ( ps -> y = z ) ) )
5	4	cbvalvw	|- ( A. x ( ph -> x = z ) <-> A. y ( ps -> y = z ) )
6	5	biimpi	|- ( A. x ( ph -> x = z ) -> A. y ( ps -> y = z ) )
7		pm2.27	|- ( ph -> ( ( ph -> x = z ) -> x = z ) )
8		pm2.27	|- ( ps -> ( ( ps -> y = z ) -> y = z ) )
9	7 8	im2anan9	|- ( ( ph /\ ps ) -> ( ( ( ph -> x = z ) /\ ( ps -> y = z ) ) -> ( x = z /\ y = z ) ) )
10		equtr2	|- ( ( x = z /\ y = z ) -> x = y )
11	9 10	syl6com	|- ( ( ( ph -> x = z ) /\ ( ps -> y = z ) ) -> ( ( ph /\ ps ) -> x = y ) )
12	11	ex	|- ( ( ph -> x = z ) -> ( ( ps -> y = z ) -> ( ( ph /\ ps ) -> x = y ) ) )
13	12	alimdv	|- ( ( ph -> x = z ) -> ( A. y ( ps -> y = z ) -> A. y ( ( ph /\ ps ) -> x = y ) ) )
14	13	com12	|- ( A. y ( ps -> y = z ) -> ( ( ph -> x = z ) -> A. y ( ( ph /\ ps ) -> x = y ) ) )
15	14	alimdv	|- ( A. y ( ps -> y = z ) -> ( A. x ( ph -> x = z ) -> A. x A. y ( ( ph /\ ps ) -> x = y ) ) )
16	6 15	mpcom	|- ( A. x ( ph -> x = z ) -> A. x A. y ( ( ph /\ ps ) -> x = y ) )
17	16	exlimiv	|- ( E. z A. x ( ph -> x = z ) -> A. x A. y ( ( ph /\ ps ) -> x = y ) )
18	2 17	sylbi	|- ( E* x ph -> A. x A. y ( ( ph /\ ps ) -> x = y ) )
19	1	cbvexvw	|- ( E. x ph <-> E. y ps )
20	19	biimpri	|- ( E. y ps -> E. x ph )
21		ax6evr	|- E. z x = z
22		pm3.2	|- ( ph -> ( ps -> ( ph /\ ps ) ) )
23	22	imim1d	|- ( ph -> ( ( ( ph /\ ps ) -> x = y ) -> ( ps -> x = y ) ) )
24		ax7	|- ( x = y -> ( x = z -> y = z ) )
25	23 24	syl8	|- ( ph -> ( ( ( ph /\ ps ) -> x = y ) -> ( ps -> ( x = z -> y = z ) ) ) )
26	25	com4r	|- ( x = z -> ( ph -> ( ( ( ph /\ ps ) -> x = y ) -> ( ps -> y = z ) ) ) )
27	26	impcom	|- ( ( ph /\ x = z ) -> ( ( ( ph /\ ps ) -> x = y ) -> ( ps -> y = z ) ) )
28	27	alimdv	|- ( ( ph /\ x = z ) -> ( A. y ( ( ph /\ ps ) -> x = y ) -> A. y ( ps -> y = z ) ) )
29	28	impancom	|- ( ( ph /\ A. y ( ( ph /\ ps ) -> x = y ) ) -> ( x = z -> A. y ( ps -> y = z ) ) )
30	29	eximdv	|- ( ( ph /\ A. y ( ( ph /\ ps ) -> x = y ) ) -> ( E. z x = z -> E. z A. y ( ps -> y = z ) ) )
31	21 30	mpi	|- ( ( ph /\ A. y ( ( ph /\ ps ) -> x = y ) ) -> E. z A. y ( ps -> y = z ) )
32		df-mo	|- ( E* y ps <-> E. z A. y ( ps -> y = z ) )
33	31 32	sylibr	|- ( ( ph /\ A. y ( ( ph /\ ps ) -> x = y ) ) -> E* y ps )
34	33	expcom	|- ( A. y ( ( ph /\ ps ) -> x = y ) -> ( ph -> E* y ps ) )
35	34	aleximi	|- ( A. x A. y ( ( ph /\ ps ) -> x = y ) -> ( E. x ph -> E. x E* y ps ) )
36		ax5e	|- ( E. x E* y ps -> E* y ps )
37	20 35 36	syl56	|- ( A. x A. y ( ( ph /\ ps ) -> x = y ) -> ( E. y ps -> E* y ps ) )
38	5	exbii	|- ( E. z A. x ( ph -> x = z ) <-> E. z A. y ( ps -> y = z ) )
39	38 2 32	3bitr4i	|- ( E* x ph <-> E* y ps )
40		moabs	|- ( E* y ps <-> ( E. y ps -> E* y ps ) )
41	39 40	bitri	|- ( E* x ph <-> ( E. y ps -> E* y ps ) )
42	37 41	sylibr	|- ( A. x A. y ( ( ph /\ ps ) -> x = y ) -> E* x ph )
43	18 42	impbii	|- ( E* x ph <-> A. x A. y ( ( ph /\ ps ) -> x = y ) )