Theorem mo4 2560

Description: At-most-one quantifier expressed using implicit substitution. This theorem is also a direct consequence of mo4f 2561, 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 2154. (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 2534	. . 3 ⊢ (∃*𝑥𝜑 ↔ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧))
2		mo4.1	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3		equequ1 2028	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))
4	2, 3	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝜑 → 𝑥 = 𝑧) ↔ (𝜓 → 𝑦 = 𝑧)))
5	4	cbvalvw 2039	. . . . . 6 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦(𝜓 → 𝑦 = 𝑧))
6	5	biimpi 215	. . . . 5 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑦(𝜓 → 𝑦 = 𝑧))
7		pm2.27 42	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝜑 → 𝑥 = 𝑧) → 𝑥 = 𝑧))
8	7	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 → 𝑥 = 𝑧) → 𝑥 = 𝑧))
9		pm2.27 42	. . . . . . . . . . . 12 ⊢ (𝜓 → ((𝜓 → 𝑦 = 𝑧) → 𝑦 = 𝑧))
10	9	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → ((𝜓 → 𝑦 = 𝑧) → 𝑦 = 𝑧))
11	8, 10	anim12d 609	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (((𝜑 → 𝑥 = 𝑧) ∧ (𝜓 → 𝑦 = 𝑧)) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑧)))
12		equtr2 2030	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑦)
13	11, 12	syl6com 37	. . . . . . . . 9 ⊢ (((𝜑 → 𝑥 = 𝑧) ∧ (𝜓 → 𝑦 = 𝑧)) → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
14	13	ex 413	. . . . . . . 8 ⊢ ((𝜑 → 𝑥 = 𝑧) → ((𝜓 → 𝑦 = 𝑧) → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
15	14	alimdv 1919	. . . . . . 7 ⊢ ((𝜑 → 𝑥 = 𝑧) → (∀𝑦(𝜓 → 𝑦 = 𝑧) → ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
16	15	com12 32	. . . . . 6 ⊢ (∀𝑦(𝜓 → 𝑦 = 𝑧) → ((𝜑 → 𝑥 = 𝑧) → ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
17	16	alimdv 1919	. . . . 5 ⊢ (∀𝑦(𝜓 → 𝑦 = 𝑧) → (∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
18	6, 17	mpcom 38	. . . 4 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
19	18	exlimiv 1933	. . 3 ⊢ (∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
20	1, 19	sylbi 216	. 2 ⊢ (∃*𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
21	2	cbvexvw 2040	. . . . 5 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
22	21	biimpri 227	. . . 4 ⊢ (∃𝑦𝜓 → ∃𝑥𝜑)
23		ax6evr 2018	. . . . . . . 8 ⊢ ∃𝑧 𝑥 = 𝑧
24		pm3.2 470	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
25	24	imim1d 82	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → 𝑥 = 𝑦)))
26		ax7 2019	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
27	25, 26	syl8 76	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → (𝑥 = 𝑧 → 𝑦 = 𝑧))))
28	27	com4r 94	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝜑 → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → 𝑦 = 𝑧))))
29	28	impcom 408	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → 𝑦 = 𝑧)))
30	29	alimdv 1919	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → ∀𝑦(𝜓 → 𝑦 = 𝑧)))
31	30	impancom 452	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → (𝑥 = 𝑧 → ∀𝑦(𝜓 → 𝑦 = 𝑧)))
32	31	eximdv 1920	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → (∃𝑧 𝑥 = 𝑧 → ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧)))
33	23, 32	mpi 20	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧))
34		df-mo 2534	. . . . . . 7 ⊢ (∃*𝑦𝜓 ↔ ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧))
35	33, 34	sylibr 233	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → ∃*𝑦𝜓)
36	35	expcom 414	. . . . 5 ⊢ (∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜑 → ∃*𝑦𝜓))
37	36	aleximi 1834	. . . 4 ⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑥∃*𝑦𝜓))
38		ax5e 1915	. . . 4 ⊢ (∃𝑥∃*𝑦𝜓 → ∃*𝑦𝜓)
39	22, 37, 38	syl56 36	. . 3 ⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (∃𝑦𝜓 → ∃*𝑦𝜓))
40	5	exbii 1850	. . . . 5 ⊢ (∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧) ↔ ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧))
41	40, 1, 34	3bitr4i 302	. . . 4 ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
42		moabs 2537	. . . 4 ⊢ (∃*𝑦𝜓 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
43	41, 42	bitri 274	. . 3 ⊢ (∃*𝑥𝜑 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
44	39, 43	sylibr 233	. 2 ⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → ∃*𝑥𝜑)
45	20, 44	impbii 208	1 ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1539  ∃wex 1781  ∃*wmo 2532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-mo 2534

This theorem is referenced by:  eu4  2611  moel  3398  moelOLD  3401  moeq  3702  rmo4  3725  mosneq  4842  dffun6  6553  dffun3OLD  6555  fun11  6619  brprcneu  6878  brprcneuALT  6879  dff13  7250  mpofunOLD  7529  caovmo  7640  wemoiso  7956  wemoiso2  7957  addsrmo  11064  mulsrmo  11065  summo  15659  prodmo  15876  hausflimi  23475  vitalilem3  25118  plyexmo  25817  nosupprefixmo  27192  noinfprefixmo  27193  tglineintmo  27882  ajmoi  30098  pjhthmo  30542  adjmo  31072  satfv0  34337  satfv0fun  34350  satffunlem1lem1  34381  satffunlem2lem1  34383  funtransport  34991  funray  35100  funline  35102  lineintmo  35117  cossssid4  37328  dffrege115  42714  mof0ALT  47459  mofsn  47463  f1omo  47480  thincmo  47602