Theorem wl-dfrmosb 34855

Description: An alternate definition of restricted "at most one" (df-wl-rmo 34854) using substitution. (Contributed by Wolf Lammen, 27-May-2023.)

Assertion

Ref	Expression
wl-dfrmosb	⊢ (∃*(𝑥 : 𝐴)𝜑 ↔ ∃*𝑦(𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑))

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

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem wl-dfrmosb

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		wl-dfralsb 34839	. . . 4 ⊢ (∀(𝑥 : 𝐴)(𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦(𝑦 ∈ 𝐴 → [𝑦 / 𝑥](𝜑 → 𝑥 = 𝑧)))
2		sbim 2311	. . . . . . . 8 ⊢ ([𝑦 / 𝑥](𝜑 → 𝑥 = 𝑧) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝑥 = 𝑧))
3		equsb3 2109	. . . . . . . . 9 ⊢ ([𝑦 / 𝑥]𝑥 = 𝑧 ↔ 𝑦 = 𝑧)
4	3	imbi2i 338	. . . . . . . 8 ⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝑥 = 𝑧) ↔ ([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑧))
5	2, 4	bitri 277	. . . . . . 7 ⊢ ([𝑦 / 𝑥](𝜑 → 𝑥 = 𝑧) ↔ ([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑧))
6	5	imbi2i 338	. . . . . 6 ⊢ ((𝑦 ∈ 𝐴 → [𝑦 / 𝑥](𝜑 → 𝑥 = 𝑧)) ↔ (𝑦 ∈ 𝐴 → ([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑧)))
7		impexp 453	. . . . . 6 ⊢ (((𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑) → 𝑦 = 𝑧) ↔ (𝑦 ∈ 𝐴 → ([𝑦 / 𝑥]𝜑 → 𝑦 = 𝑧)))
8	6, 7	bitr4i 280	. . . . 5 ⊢ ((𝑦 ∈ 𝐴 → [𝑦 / 𝑥](𝜑 → 𝑥 = 𝑧)) ↔ ((𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑) → 𝑦 = 𝑧))
9	8	albii 1820	. . . 4 ⊢ (∀𝑦(𝑦 ∈ 𝐴 → [𝑦 / 𝑥](𝜑 → 𝑥 = 𝑧)) ↔ ∀𝑦((𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑) → 𝑦 = 𝑧))
10	1, 9	bitri 277	. . 3 ⊢ (∀(𝑥 : 𝐴)(𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦((𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑) → 𝑦 = 𝑧))
11	10	exbii 1848	. 2 ⊢ (∃𝑧∀(𝑥 : 𝐴)(𝜑 → 𝑥 = 𝑧) ↔ ∃𝑧∀𝑦((𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑) → 𝑦 = 𝑧))
12		df-wl-rmo 34854	. 2 ⊢ (∃*(𝑥 : 𝐴)𝜑 ↔ ∃𝑧∀(𝑥 : 𝐴)(𝜑 → 𝑥 = 𝑧))
13		df-mo 2622	. 2 ⊢ (∃*𝑦(𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ ∃𝑧∀𝑦((𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑) → 𝑦 = 𝑧))
14	11, 12, 13	3bitr4i 305	1 ⊢ (∃*(𝑥 : 𝐴)𝜑 ↔ ∃*𝑦(𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535  ∃wex 1780  [wsb 2069   ∈ wcel 2114  ∃*wmo 2620  ∀wl-ral 34833  ∃*wl-rmo 34835

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  ax-10 2145  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-wl-ral 34838  df-wl-rmo 34854

This theorem is referenced by:  wl-dfreusb  34859