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