Theorem bj-vjust

Description: Justification theorem for bj-df-v . 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		df-clab	|- ( z e. { x | T. } <-> [ z / x ] T. )
2		sbv	|- ( [ z / y ] T. <-> T. )
3		df-clab	|- ( z e. { y | T. } <-> [ z / y ] T. )
4		sbv	|- ( [ z / x ] T. <-> T. )
5	2 3 4	3bitr4ri	|- ( [ z / x ] T. <-> z e. { y | T. } )
6	1 5	bitri	|- ( z e. { x | T. } <-> z e. { y | T. } )
7	6	eqriv	|- { x | T. } = { y | T. }