Theorem mo4 2592

Description: At-most-one quantifier expressed using implicit substitution. This theorem is also a direct consequence of mo4f 2593, 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 2194. (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 2566	. . 3 ⊢ (∃*𝑥𝜑 ↔ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧))
2		mo4.1	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3		equequ1 2058	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))
4	2, 3	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝜑 → 𝑥 = 𝑧) ↔ (𝜓 → 𝑦 = 𝑧)))
5	4	cbvalvw 2069	. . . . . 6 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦(𝜓 → 𝑦 = 𝑧))
6	5	biimpi 219	. . . . 5 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑦(𝜓 → 𝑦 = 𝑧))
7		pm2.27 43	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝜑 → 𝑥 = 𝑧) → 𝑥 = 𝑧))
8		pm2.27 43	. . . . . . . . . . 11 ⊢ (𝜓 → ((𝜓 → 𝑦 = 𝑧) → 𝑦 = 𝑧))
9	7, 8	im2anan9 632	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜓) → (((𝜑 → 𝑥 = 𝑧) ∧ (𝜓 → 𝑦 = 𝑧)) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑧)))
10		equtr2 2060	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑦)
11	9, 10	syl6com 38	. . . . . . . . 9 ⊢ (((𝜑 → 𝑥 = 𝑧) ∧ (𝜓 → 𝑦 = 𝑧)) → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
12	11	ex 418	. . . . . . . 8 ⊢ ((𝜑 → 𝑥 = 𝑧) → ((𝜓 → 𝑦 = 𝑧) → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
13	12	alimdv 1949	. . . . . . 7 ⊢ ((𝜑 → 𝑥 = 𝑧) → (∀𝑦(𝜓 → 𝑦 = 𝑧) → ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
14	13	com12 33	. . . . . 6 ⊢ (∀𝑦(𝜓 → 𝑦 = 𝑧) → ((𝜑 → 𝑥 = 𝑧) → ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
15	14	alimdv 1949	. . . . 5 ⊢ (∀𝑦(𝜓 → 𝑦 = 𝑧) → (∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
16	6, 15	mpcom 39	. . . 4 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
17	16	exlimiv 1963	. . 3 ⊢ (∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧) → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
18	1, 17	sylbi 220	. 2 ⊢ (∃*𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
19	2	cbvexvw 2070	. . . . 5 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
20	19	biimpri 231	. . . 4 ⊢ (∃𝑦𝜓 → ∃𝑥𝜑)
21		ax6evr 2048	. . . . . . . 8 ⊢ ∃𝑧 𝑥 = 𝑧
22		pm3.2 475	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
23	22	imim1d 83	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → 𝑥 = 𝑦)))
24		ax7 2049	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
25	23, 24	syl8 77	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → (𝑥 = 𝑧 → 𝑦 = 𝑧))))
26	25	com4r 95	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝜑 → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → 𝑦 = 𝑧))))
27	26	impcom 413	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜓 → 𝑦 = 𝑧)))
28	27	alimdv 1949	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 = 𝑧) → (∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → ∀𝑦(𝜓 → 𝑦 = 𝑧)))
29	28	impancom 457	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → (𝑥 = 𝑧 → ∀𝑦(𝜓 → 𝑦 = 𝑧)))
30	29	eximdv 1950	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → (∃𝑧 𝑥 = 𝑧 → ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧)))
31	21, 30	mpi 21	. . . . . . 7 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧))
32		dfmo 2566	. . . . . . 7 ⊢ (∃*𝑦𝜓 ↔ ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧))
33	31, 32	sylibr 237	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) → ∃*𝑦𝜓)
34	33	expcom 419	. . . . 5 ⊢ (∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (𝜑 → ∃*𝑦𝜓))
35	34	aleximi 1865	. . . 4 ⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑥∃*𝑦𝜓))
36		ax5e 1945	. . . 4 ⊢ (∃𝑥∃*𝑦𝜓 → ∃*𝑦𝜓)
37	20, 35, 36	syl56 37	. . 3 ⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → (∃𝑦𝜓 → ∃*𝑦𝜓))
38	5	exbii 1881	. . . . 5 ⊢ (∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧) ↔ ∃𝑧∀𝑦(𝜓 → 𝑦 = 𝑧))
39	38, 1, 32	3bitr4i 306	. . . 4 ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
40		moabs 2569	. . . 4 ⊢ (∃*𝑦𝜓 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
41	39, 40	bitri 278	. . 3 ⊢ (∃*𝑥𝜑 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
42	37, 41	sylibr 237	. 2 ⊢ (∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) → ∃*𝑥𝜑)
43	18, 42	impbii 212	1 ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568  ∃wex 1812  ∃*wmo 2563

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2565

This theorem is used by:  eu4  2641  moel  3386  moeq  3665  rmo4  3688  mosneq  4802  dffun6  6549  fun11  6614  brprcneu  6875  brprcneuALT  6876  dff13  7258  caovmo  7658  wemoiso  7985  wemoiso2  7986  addsrmo  11158  mulsrmo  11159  summo  15883  prodmo  16103  hausflimi  24299  vitalilem3  25931  plyexmo  26636  nosupprefixmo  28057  noinfprefixmo  28058  tglineintmo  29110  ajmoi  31460  pjhthmo  31904  adjmo  32434  satfv0  36123  satfv0fun  36136  satffunlem1lem1  36167  satffunlem2lem1  36169  funtransport  36796  funray  36905  funline  36907  lineintmo  36922  mopre  39403  cossssid4  39492  dffrege115  44977  mof0ALT  49949  mofsn  49953  f1omoOLD  50001  thincmo  50535  euendfunc  50633