Theorem rmo4 3752

Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by NM, 16-Jun-2017.)

Hypothesis

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

Assertion

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

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

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

Proof of Theorem rmo4

Step	Hyp	Ref	Expression
1		df-rmo 3388	. 2 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		an4 655	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐴 ∧ 𝜓)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝜑 ∧ 𝜓)))
3		ancom 460	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴))
4	2, 3	bianbi 626	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐴 ∧ 𝜓)) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝜑 ∧ 𝜓)))
5	4	imbi1i 349	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐴 ∧ 𝜓)) → 𝑥 = 𝑦) ↔ (((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝜑 ∧ 𝜓)) → 𝑥 = 𝑦))
6		impexp 450	. . . . . . 7 ⊢ ((((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝜑 ∧ 𝜓)) → 𝑥 = 𝑦) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
7		impexp 450	. . . . . . 7 ⊢ (((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) ↔ (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝐴 → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))))
8	5, 6, 7	3bitri 297	. . . . . 6 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐴 ∧ 𝜓)) → 𝑥 = 𝑦) ↔ (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝐴 → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))))
9	8	albii 1817	. . . . 5 ⊢ (∀𝑦(((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐴 ∧ 𝜓)) → 𝑥 = 𝑦) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑥 ∈ 𝐴 → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))))
10		df-ral 3068	. . . . 5 ⊢ (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝐴 → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑥 ∈ 𝐴 → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))))
11		r19.21v 3186	. . . . 5 ⊢ (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝐴 → ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
12	9, 10, 11	3bitr2i 299	. . . 4 ⊢ (∀𝑦(((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐴 ∧ 𝜓)) → 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
13	12	albii 1817	. . 3 ⊢ (∀𝑥∀𝑦(((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐴 ∧ 𝜓)) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
14		eleq1w 2827	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
15		rmo4.1	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
16	14, 15	anbi12d 631	. . . 4 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
17	16	mo4 2569	. . 3 ⊢ (∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥∀𝑦(((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐴 ∧ 𝜓)) → 𝑥 = 𝑦))
18		df-ral 3068	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
19	13, 17, 18	3bitr4i 303	. 2 ⊢ (∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
20	1, 19	bitri 275	1 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535   ∈ wcel 2108  ∃*wmo 2541  ∀wral 3067  ∃*wrmo 3387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-mo 2543  df-clel 2819  df-ral 3068  df-rmo 3388

This theorem is referenced by:  reu4  3753  disjor  5148  somo  5646  nnasmo  8719  supmo  9521  infmo  9564  sqrmo  15300  catideu  17733  poslubmo  18481  posglbmo  18482  mgmidmo  18698  mndinvmod  18802  lspextmo  21078  evlseu  22130  ply1divmo  26195  2sqmo  27499  divsmo  28228  tghilberti2  28664  foot  28748  mideu  28764  cvmliftmo  35252  r1peuqusdeg1  35611  hilbert1.2  36119  poimirlem1  37581  poimirlem13  37593  poimirlem14  37594  poimirlem18  37598  poimirlem21  37601  inecmo  38311  idomsubgmo  43154