Theorem vexwt

Description: A standard theorem of predicate calculus ( stdpc4 ) expressed using class abstractions. Closed form of vexw . (Contributed by BJ, 14-Jun-2019)

	Ref	Expression
Assertion	vexwt	$$⊢\forall x\phi \to y\in \left\{x|\phi \right\}$$

Proof

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