Theorem mo4 2646

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

By the way, swapping 𝑥, 𝑦 and 𝜑, 𝜓 leads to an expression for ∃*𝑦𝜓, which is equivalent to ∃*𝑥𝜑 (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 2157. (Contributed by NM, 26-Jul-1995.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2023.)

Hypothesis

Ref	Expression
mo4.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
mo4	⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem mo4

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-mo 2618	. . 3 ⊢ (∃*𝑥𝜑 ↔ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧))
2		mo4.1	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3		equequ1 2028	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))
4	2, 3	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝜑 → 𝑥 = 𝑧) ↔ (𝜓 → 𝑦 = 𝑧)))
5	4	cbvalvw 2039	. . . . . 6 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦(𝜓 → 𝑦 = 𝑧))
6	5	biimpi 218	. . . . 5 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑦(𝜓 → 𝑦 = 𝑧))
7		pm2.27 42	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝜑 → 𝑥 = 𝑧) → 𝑥 = 𝑧))
8	7	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 → 𝑥 = 𝑧) → 𝑥 = 𝑧))
9		pm2.27 42	. . . . . . . . . . . 12 ⊢ (𝜓 → ((𝜓 → 𝑦 = 𝑧) → 𝑦 = 𝑧))
10	9	adantl 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ((𝜓 → 𝑦 = 𝑧) → 𝑦 = 𝑧))
11	8, 10	anim12d 610	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (((𝜑 → 𝑥 = 𝑧) ∧ (𝜓 → 𝑦 = 𝑧)) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑧)))
12		equtr2 2030	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑦)
13	11, 12	syl6com 37	. . . . . . . . 9 ⊢ (((𝜑 → 𝑥 = 𝑧) ∧ (𝜓 → 𝑦 = 𝑧)) → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
14	13	ex 415	. . . . . . . 8 ⊢ ((𝜑 → 𝑥 = 𝑧) → ((𝜓 → 𝑦 = 𝑧) → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
15	14	alimdv 1913	. . . . . . 7 ⊢ ((𝜑 → 𝑥 = 𝑧) → (∀𝑦(𝜓 → 𝑦 = 𝑧) → ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
16	15	com12 32	. . . . . 6 ⊢ (∀𝑦(𝜓 → 𝑦 = 𝑧) → ((𝜑 → 𝑥 = 𝑧) → ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
17	16	alimdv 1913	. . . . 5 ⊢ (∀𝑦(𝜓 → 𝑦 = 𝑧) → (∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
18	6, 17	mpcom 38	. . . 4 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
19	18	exlimiv 1927	. . 3 ⊢ (∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
20	1, 19	sylbi 219	. 2 ⊢ (∃*𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
21	2	cbvexvw 2040	. . . . 5 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
22	21	biimpri 230	. . . 4 ⊢ (∃𝑦𝜓 → ∃𝑥𝜑)
23		ax6evr 2018	. . . . . . . 8 ⊢ ∃𝑧 𝑥 = 𝑧
24		pm3.2 472	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
25	24	imim1d 82	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → 𝑥 = 𝑦)))
26		ax7 2019	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
27	25, 26	syl8 76	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → (𝑥 = 𝑧 → 𝑦 = 𝑧))))
28	27	com4r 94	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝜑 → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → 𝑦 = 𝑧))))
29	28	impcom 410	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → 𝑦 = 𝑧)))
30	29	alimdv 1913	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → ∀𝑦(𝜓 → 𝑦 = 𝑧)))
31	30	impancom 454	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → (𝑥 = 𝑧 → ∀𝑦(𝜓 → 𝑦 = 𝑧)))
32	31	eximdv 1914	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → (∃𝑧 𝑥 = 𝑧 → ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧)))
33	23, 32	mpi 20	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧))
34		df-mo 2618	. . . . . . 7 ⊢ (∃*𝑦𝜓 ↔ ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧))
35	33, 34	sylibr 236	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → ∃*𝑦𝜓)
36	35	expcom 416	. . . . 5 ⊢ (∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜑 → ∃*𝑦𝜓))
37	36	aleximi 1828	. . . 4 ⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑥∃*𝑦𝜓))
38		ax5e 1909	. . . 4 ⊢ (∃𝑥∃*𝑦𝜓 → ∃*𝑦𝜓)
39	22, 37, 38	syl56 36	. . 3 ⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (∃𝑦𝜓 → ∃*𝑦𝜓))
40	5	exbii 1844	. . . . 5 ⊢ (∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧) ↔ ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧))
41	40, 1, 34	3bitr4i 305	. . . 4 ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
42		moabs 2621	. . . 4 ⊢ (∃*𝑦𝜓 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
43	41, 42	bitri 277	. . 3 ⊢ (∃*𝑥𝜑 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
44	39, 43	sylibr 236	. 2 ⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → ∃*𝑥𝜑)
45	20, 44	impbii 211	1 ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1531  ∃wex 1776  ∃*wmo 2616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-mo 2618

This theorem is referenced by:  eu4  2695  moeq  3697  rmo4  3720  mosneq  4772  dffun3  6365  fun11  6427  brprcneu  6661  dff13  7012  mpofun  7275  caovmo  7384  wemoiso  7673  wemoiso2  7674  addsrmo  10494  mulsrmo  10495  summo  15073  prodmo  15289  hausflimi  22587  vitalilem3  24210  plyexmo  24901  tglineintmo  26427  ajmoi  28634  pjhthmo  29078  adjmo  29608  moel  30251  satfv0  32605  satfv0fun  32618  satffunlem1lem1  32649  satffunlem2lem1  32651  noprefixmo  33202  funtransport  33492  funray  33601  funline  33603  lineintmo  33618  cossssid4  35709  dffrege115  40322