Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-mo Structured version   Visualization version   GIF version

Definition df-bj-mo 33152
 Description: Definition of the uniqueness quantifier which is correct on the empty domain. Instead of the fresh variable 𝑧, one could save a dummy variable by using 𝑥 or 𝑦 at the cost of having nested quantifiers on the same variable. (Contributed by BJ, 12-Mar-2023.)
Assertion
Ref Expression
df-bj-mo (∃**𝑥𝜑 ↔ ∀𝑧𝑦𝑥(𝜑𝑥 = 𝑦))
Distinct variable groups:   𝑥,𝑦,𝑧   𝜑,𝑦,𝑧
Allowed substitution hint:   𝜑(𝑥)

Detailed syntax breakdown of Definition df-bj-mo
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
31, 2wmoo 33151 . 2 wff ∃**𝑥𝜑
4 vy . . . . . . 7 setvar 𝑦
52, 4weq 2061 . . . . . 6 wff 𝑥 = 𝑦
61, 5wi 4 . . . . 5 wff (𝜑𝑥 = 𝑦)
76, 2wal 1654 . . . 4 wff 𝑥(𝜑𝑥 = 𝑦)
87, 4wex 1878 . . 3 wff 𝑦𝑥(𝜑𝑥 = 𝑦)
9 vz . . 3 setvar 𝑧
108, 9wal 1654 . 2 wff 𝑧𝑦𝑥(𝜑𝑥 = 𝑦)
113, 10wb 198 1 wff (∃**𝑥𝜑 ↔ ∀𝑧𝑦𝑥(𝜑𝑥 = 𝑦))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator