Theorem mo4 2594

Description: At-most-one quantifier expressed using implicit substitution. This theorem is also a direct consequence of mo4f 2595, 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 2192. (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		dfmo 2568	. . 3 ⊢ (∃*𝑥𝜑 ↔ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧))
2		mo4.1	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3		equequ1 2046	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))
4	2, 3	imbi12d 346	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝜑 → 𝑥 = 𝑧) ↔ (𝜓 → 𝑦 = 𝑧)))
5	4	cbvalvw 2057	. . . . . 6 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦(𝜓 → 𝑦 = 𝑧))
6	5	biimpi 218	. . . . 5 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑦(𝜓 → 𝑦 = 𝑧))
7		pm2.27 42	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝜑 → 𝑥 = 𝑧) → 𝑥 = 𝑧))
8		pm2.27 42	. . . . . . . . . . 11 ⊢ (𝜓 → ((𝜓 → 𝑦 = 𝑧) → 𝑦 = 𝑧))
9	7, 8	im2anan9 629	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (((𝜑 → 𝑥 = 𝑧) ∧ (𝜓 → 𝑦 = 𝑧)) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑧)))
10		equtr2 2048	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑦)
11	9, 10	syl6com 37	. . . . . . . . 9 ⊢ (((𝜑 → 𝑥 = 𝑧) ∧ (𝜓 → 𝑦 = 𝑧)) → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
12	11	ex 416	. . . . . . . 8 ⊢ ((𝜑 → 𝑥 = 𝑧) → ((𝜓 → 𝑦 = 𝑧) → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
13	12	alimdv 1937	. . . . . . 7 ⊢ ((𝜑 → 𝑥 = 𝑧) → (∀𝑦(𝜓 → 𝑦 = 𝑧) → ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
14	13	com12 32	. . . . . 6 ⊢ (∀𝑦(𝜓 → 𝑦 = 𝑧) → ((𝜑 → 𝑥 = 𝑧) → ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
15	14	alimdv 1937	. . . . 5 ⊢ (∀𝑦(𝜓 → 𝑦 = 𝑧) → (∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
16	6, 15	mpcom 38	. . . 4 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
17	16	exlimiv 1951	. . 3 ⊢ (∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
18	1, 17	sylbi 219	. 2 ⊢ (∃*𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
19	2	cbvexvw 2058	. . . . 5 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
20	19	biimpri 230	. . . 4 ⊢ (∃𝑦𝜓 → ∃𝑥𝜑)
21		ax6evr 2036	. . . . . . . 8 ⊢ ∃𝑧 𝑥 = 𝑧
22		pm3.2 473	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
23	22	imim1d 82	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → 𝑥 = 𝑦)))
24		ax7 2037	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
25	23, 24	syl8 76	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → (𝑥 = 𝑧 → 𝑦 = 𝑧))))
26	25	com4r 94	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝜑 → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → 𝑦 = 𝑧))))
27	26	impcom 411	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → 𝑦 = 𝑧)))
28	27	alimdv 1937	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → ∀𝑦(𝜓 → 𝑦 = 𝑧)))
29	28	impancom 455	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → (𝑥 = 𝑧 → ∀𝑦(𝜓 → 𝑦 = 𝑧)))
30	29	eximdv 1938	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → (∃𝑧 𝑥 = 𝑧 → ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧)))
31	21, 30	mpi 20	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧))
32		dfmo 2568	. . . . . . 7 ⊢ (∃*𝑦𝜓 ↔ ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧))
33	31, 32	sylibr 236	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → ∃*𝑦𝜓)
34	33	expcom 417	. . . . 5 ⊢ (∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜑 → ∃*𝑦𝜓))
35	34	aleximi 1853	. . . 4 ⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑥∃*𝑦𝜓))
36		ax5e 1933	. . . 4 ⊢ (∃𝑥∃*𝑦𝜓 → ∃*𝑦𝜓)
37	20, 35, 36	syl56 36	. . 3 ⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (∃𝑦𝜓 → ∃*𝑦𝜓))
38	5	exbii 1869	. . . . 5 ⊢ (∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧) ↔ ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧))
39	38, 1, 32	3bitr4i 305	. . . 4 ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
40		moabs 2571	. . . 4 ⊢ (∃*𝑦𝜓 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
41	39, 40	bitri 277	. . 3 ⊢ (∃*𝑥𝜑 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
42	37, 41	sylibr 236	. 2 ⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → ∃*𝑥𝜑)
43	18, 42	impbii 211	1 ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1559  ∃wex 1800  ∃*wmo 2565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-mo 2567

This theorem is referenced by:  eu4  2643  moel  3388  moeq  3671  rmo4  3694  mosneq  4801  dffun6  6533  fun11  6596  brprcneu  6858  brprcneuALT  6859  dff13  7239  caovmo  7634  wemoiso  7955  wemoiso2  7956  addsrmo  11032  mulsrmo  11033  summo  15745  prodmo  15967  hausflimi  24041  vitalilem3  25673  plyexmo  26378  nosupprefixmo  27765  noinfprefixmo  27766  tglineintmo  28812  ajmoi  31062  pjhthmo  31506  adjmo  32036  satfv0  35709  satfv0fun  35722  satffunlem1lem1  35753  satffunlem2lem1  35755  funtransport  36382  funray  36491  funline  36493  lineintmo  36508  mopre  38971  cossssid4  39060  dffrege115  44555  mof0ALT  49462  mofsn  49466  f1omoOLD  49516  thincmo  50050  euendfunc  50148