Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-wl-rmo Structured version   Visualization version   GIF version

Definition df-wl-rmo 34733
Description: Restrict "at most one" to a given class 𝐴. This version does not interpret elementhood verbatim like ∃*𝑥𝐴𝜑 does. Assuming a real elementhood can lead to awkward consequences should the class 𝐴 depend on 𝑥. Instead we base the definition on df-wl-ral 34717, where this is already ruled out.

This definition lets 𝑥 appear as a formal parameter with no connection to 𝐴, but occurrences in 𝜑 are fully honored.

Alternate definitions are given in wl-dfrmosb 34734 and, if 𝑥 is not free in 𝐴, wl-dfrmov 34735 and wl-dfrmof 34736. (Contributed by NM, 30-Aug-1993.) Isolate x from A. (Revised by Wolf Lammen, 26-May-2023.)

Assertion
Ref Expression
df-wl-rmo (∃*(𝑥 : 𝐴)𝜑 ↔ ∃𝑦∀(𝑥 : 𝐴)(𝜑𝑥 = 𝑦))
Distinct variable groups:   𝑥,𝑦   𝜑,𝑦   𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Detailed syntax breakdown of Definition df-wl-rmo
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wl-rmo 34714 . 2 wff ∃*(𝑥 : 𝐴)𝜑
5 vy . . . . . 6 setvar 𝑦
62, 5weq 1955 . . . . 5 wff 𝑥 = 𝑦
71, 6wi 4 . . . 4 wff (𝜑𝑥 = 𝑦)
87, 2, 3wl-ral 34712 . . 3 wff ∀(𝑥 : 𝐴)(𝜑𝑥 = 𝑦)
98, 5wex 1771 . 2 wff 𝑦∀(𝑥 : 𝐴)(𝜑𝑥 = 𝑦)
104, 9wb 207 1 wff (∃*(𝑥 : 𝐴)𝜑 ↔ ∃𝑦∀(𝑥 : 𝐴)(𝜑𝑥 = 𝑦))
Colors of variables: wff setvar class
This definition is referenced by:  wl-dfrmosb  34734  wl-dfrmov  34735  wl-dfrmof  34736
  Copyright terms: Public domain W3C validator