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 34708
Description: Variant of df-clab 2797, 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 2790, df-clel 2890 and df-cleq 2811. 𝑥𝐴 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 2107, ax-9 2115, or df-clel 2890. Theorem cleljust 2114 shows that a possible choice does not matter.

The original df-clab 2797 can be rederived, see wl-dfclab 34709. 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 2797 1 (𝑥 ∈ {𝑦𝜑} ↔ [𝑥 / 𝑦]𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 207  [wsb 2060  wcel 2105  {cab 2796
This theorem depends on definitions:  df-clab 2797
This theorem is referenced by:  wl-dfclab  34709
  Copyright terms: Public domain W3C validator