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

Definition df-wl-clelv2 33807
Description: Define the term 𝑥𝐴, 𝑥 in 𝐴 permitted. (Contributed by Wolf Lammen, 27-Nov-2021.)
Assertion
Ref Expression
df-wl-clelv2 (𝑥𝐴 ↔ ∀𝑢(𝑢 = 𝑥𝑢𝐴))
Distinct variable groups:   𝑢,𝐴   𝑥,𝑢
Allowed substitution hint:   𝐴(𝑥)

Detailed syntax breakdown of Definition df-wl-clelv2
StepHypRef Expression
1 vx . . 3 setvar 𝑥
2 cA . . 3 class 𝐴
31, 2wcel2-wl 33802 . 2 wff 𝑥𝐴
4 vu . . . . 5 setvar 𝑢
54, 1weq 2056 . . . 4 wff 𝑢 = 𝑥
64, 2wcel-wl 33800 . . . 4 wff 𝑢𝐴
75, 6wi 4 . . 3 wff (𝑢 = 𝑥𝑢𝐴)
87, 4wal 1650 . 2 wff 𝑢(𝑢 = 𝑥𝑢𝐴)
93, 8wb 197 1 wff (𝑥𝐴 ↔ ∀𝑢(𝑢 = 𝑥𝑢𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  wl-ax8clv2  33808
  Copyright terms: Public domain W3C validator