Description: Variant of df-clab , where the element x 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 , df-clel and df-cleq . x e. A with A depending on x 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 x e. A with x , A not disjoint, is now only introduced either via ax-8 , ax-9 , or df-clel . Theorem cleljust shows that a possible choice does not matter.
The original df-clab can be rederived, see wl-dfclab . 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)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-clabv | |- ( x e. { y | ph } <-> [ x / y ] ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-clab | |- ( x e. { y | ph } <-> [ x / y ] ph ) |