Theorem bj-vjust

Description: Justification theorem for dfv2 if it were the definition. See also vjust . (Contributed by BJ, 30-Nov-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-vjust	|- { x | T. } = { y | T. }

Proof

Step	Hyp	Ref	Expression
1		vextru	|- z e. { x | T. }
2		vextru	|- z e. { y | T. }
3	1 2	2th	|- ( z e. { x | T. } <-> z e. { y | T. } )
4	3	eqriv	|- { x | T. } = { y | T. }