Metamath Proof Explorer


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φψ
Assertion mo4 *xφxyφψx=y

Proof

Step Hyp Ref Expression
1 mo4.1 x=yφψ
2 df-mo *xφzxφx=z
3 equequ1 x=yx=zy=z
4 1 3 imbi12d x=yφx=zψy=z
5 4 cbvalvw xφx=zyψy=z
6 5 biimpi xφx=zyψy=z
7 pm2.27 φφx=zx=z
8 7 adantr φψφx=zx=z
9 pm2.27 ψψy=zy=z
10 9 adantl φψψy=zy=z
11 8 10 anim12d φψφx=zψy=zx=zy=z
12 equtr2 x=zy=zx=y
13 11 12 syl6com φx=zψy=zφψx=y
14 13 ex φx=zψy=zφψx=y
15 14 alimdv φx=zyψy=zyφψx=y
16 15 com12 yψy=zφx=zyφψx=y
17 16 alimdv yψy=zxφx=zxyφψx=y
18 6 17 mpcom xφx=zxyφψx=y
19 18 exlimiv zxφx=zxyφψx=y
20 2 19 sylbi *xφxyφψx=y
21 1 cbvexvw xφyψ
22 21 biimpri yψxφ
23 ax6evr zx=z
24 pm3.2 φψφψ
25 24 imim1d φφψx=yψx=y
26 ax7 x=yx=zy=z
27 25 26 syl8 φφψx=yψx=zy=z
28 27 com4r x=zφφψx=yψy=z
29 28 impcom φx=zφψx=yψy=z
30 29 alimdv φx=zyφψx=yyψy=z
31 30 impancom φyφψx=yx=zyψy=z
32 31 eximdv φyφψx=yzx=zzyψy=z
33 23 32 mpi φyφψx=yzyψy=z
34 df-mo *yψzyψy=z
35 33 34 sylibr φyφψx=y*yψ
36 35 expcom yφψx=yφ*yψ
37 36 aleximi xyφψx=yxφx*yψ
38 ax5e x*yψ*yψ
39 22 37 38 syl56 xyφψx=yyψ*yψ
40 5 exbii zxφx=zzyψy=z
41 40 2 34 3bitr4i *xφ*yψ
42 moabs *yψyψ*yψ
43 41 42 bitri *xφyψ*yψ
44 39 43 sylibr xyφψx=y*xφ
45 20 44 impbii *xφxyφψx=y