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	|- ( A. x ph -> y e. { x | ph } )

Proof

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