Theorem wl-clabv 38436

Description: Variant of df-clab 2739, 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 2732, df-clel 2835 and df-cleq 2752. 𝑥 ∈ 𝐴 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 2147, ax-9 2155, or df-clel 2835. Theorem cleljust 2154 shows that a possible choice does not matter.

The original df-clab 2739 can be rederived, see wl-dfclab 38437. 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

Step	Hyp	Ref	Expression
1		df-clab 2739	1 ⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)

This proof depends on syntax axioms:   ↔ wb 209  [wsb 2099   ∈ wcel 2145  {cab 2738

This proof depends on definitions:  df-clab 2739

This theorem is used by:  wl-dfclab  38437