Theorem mo4 2650

Description: At-most-one quantifier expressed using implicit substitution. This theorem is also a direct consequence of mo4f 2651, 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 2161. (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 2622	. . 3 ⊢ (∃*𝑥𝜑 ↔ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧))
2		mo4.1	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3		equequ1 2032	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))
4	2, 3	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝜑 → 𝑥 = 𝑧) ↔ (𝜓 → 𝑦 = 𝑧)))
5	4	cbvalvw 2043	. . . . . 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 2034	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑦)
13	11, 12	syl6com 37	. . . . . . . . 9 ⊢ (((𝜑 → 𝑥 = 𝑧) ∧ (𝜓 → 𝑦 = 𝑧)) → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
14	13	ex 415	. . . . . . . 8 ⊢ ((𝜑 → 𝑥 = 𝑧) → ((𝜓 → 𝑦 = 𝑧) → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
15	14	alimdv 1917	. . . . . . 7 ⊢ ((𝜑 → 𝑥 = 𝑧) → (∀𝑦(𝜓 → 𝑦 = 𝑧) → ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
16	15	com12 32	. . . . . 6 ⊢ (∀𝑦(𝜓 → 𝑦 = 𝑧) → ((𝜑 → 𝑥 = 𝑧) → ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
17	16	alimdv 1917	. . . . 5 ⊢ (∀𝑦(𝜓 → 𝑦 = 𝑧) → (∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
18	6, 17	mpcom 38	. . . 4 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
19	18	exlimiv 1931	. . 3 ⊢ (∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
20	1, 19	sylbi 219	. 2 ⊢ (∃*𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
21	2	cbvexvw 2044	. . . . 5 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
22	21	biimpri 230	. . . 4 ⊢ (∃𝑦𝜓 → ∃𝑥𝜑)
23		ax6evr 2022	. . . . . . . 8 ⊢ ∃𝑧 𝑥 = 𝑧
24		pm3.2 472	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
25	24	imim1d 82	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → 𝑥 = 𝑦)))
26		ax7 2023	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
27	25, 26	syl8 76	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → (𝑥 = 𝑧 → 𝑦 = 𝑧))))
28	27	com4r 94	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝜑 → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → 𝑦 = 𝑧))))
29	28	impcom 410	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → 𝑦 = 𝑧)))
30	29	alimdv 1917	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → ∀𝑦(𝜓 → 𝑦 = 𝑧)))
31	30	impancom 454	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → (𝑥 = 𝑧 → ∀𝑦(𝜓 → 𝑦 = 𝑧)))
32	31	eximdv 1918	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → (∃𝑧 𝑥 = 𝑧 → ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧)))
33	23, 32	mpi 20	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧))
34		df-mo 2622	. . . . . . 7 ⊢ (∃*𝑦𝜓 ↔ ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧))
35	33, 34	sylibr 236	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → ∃*𝑦𝜓)
36	35	expcom 416	. . . . 5 ⊢ (∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜑 → ∃*𝑦𝜓))
37	36	aleximi 1832	. . . 4 ⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑥∃*𝑦𝜓))
38		ax5e 1913	. . . 4 ⊢ (∃𝑥∃*𝑦𝜓 → ∃*𝑦𝜓)
39	22, 37, 38	syl56 36	. . 3 ⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (∃𝑦𝜓 → ∃*𝑦𝜓))
40	5	exbii 1848	. . . . 5 ⊢ (∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧) ↔ ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧))
41	40, 1, 34	3bitr4i 305	. . . 4 ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
42		moabs 2625	. . . 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 1535  ∃wex 1780  ∃*wmo 2620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-mo 2622

This theorem is referenced by:  eu4  2699  moeq  3700  rmo4  3723  mosneq  4775  dffun3  6368  fun11  6430  brprcneu  6664  dff13  7015  mpofun  7278  caovmo  7387  wemoiso  7676  wemoiso2  7677  addsrmo  10497  mulsrmo  10498  summo  15076  prodmo  15292  hausflimi  22590  vitalilem3  24213  plyexmo  24904  tglineintmo  26430  ajmoi  28637  pjhthmo  29081  adjmo  29611  moel  30254  satfv0  32607  satfv0fun  32620  satffunlem1lem1  32651  satffunlem2lem1  32653  noprefixmo  33204  funtransport  33494  funray  33603  funline  33605  lineintmo  33620  cossssid4  35712  dffrege115  40331