Metamath Proof Explorer


Theorem wl-clabv

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 )

Proof

Step Hyp Ref Expression
1 df-clab
 |-  ( x e. { y | ph } <-> [ x / y ] ph )