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\in \left\{y|\phi \right\}\leftrightarrow \left[x/y\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		df-clab	$$⊢x\in \left\{y|\phi \right\}\leftrightarrow \left[x/y\right]\phi$$