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

Theorem wl-clabv 36760
Description: Variant of df-clab 2708, where the element 𝑥 is required to be disjoint from the class it is taken from. This restriction meets similar ones found in other definitions and axioms like ax-ext 2701, df-clel 2808 and df-cleq 2722. 𝑥𝐴 with 𝐴 depending on 𝑥 can be the source of side effects, that you rather want to be aware of. So here we eliminate one possible way of letting this slip in instead.

An expression 𝑥𝐴 with 𝑥, 𝐴 not disjoint, is now only introduced either via ax-8 2106, ax-9 2114, or df-clel 2808. Theorem cleljust 2113 shows that a possible choice does not matter.

The original df-clab 2708 can be rederived, see wl-dfclab 36761. In an implementation this theorem is the only user of df-clab. (Contributed by NM, 26-May-1993.) Element and class are disjoint. (Revised by Wolf Lammen, 31-May-2023.)

Assertion
Ref Expression
wl-clabv (𝑥 ∈ {𝑦𝜑} ↔ [𝑥 / 𝑦]𝜑)
Distinct variable groups:   𝑥,𝑦   𝜑,𝑥
Allowed substitution hint:   𝜑(𝑦)

Proof of Theorem wl-clabv
StepHypRef Expression
1 df-clab 2708 1 (𝑥 ∈ {𝑦𝜑} ↔ [𝑥 / 𝑦]𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 205  [wsb 2065  wcel 2104  {cab 2707
This theorem depends on definitions:  df-clab 2708
This theorem is referenced by:  wl-dfclab  36761
  Copyright terms: Public domain W3C validator