Description: Variant of df-clab 2715, 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 2708,
df-clel 2815 and df-cleq 2729. 𝑥 ∈ 𝐴 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 2109, ax-9 2117, or df-clel 2815. Theorem
cleljust 2116 shows that a possible choice does not matter.
The original df-clab 2715 can be rederived, see wl-dfclab 36077. 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.) |