Theorem sa-abvi

Description: A theorem about the universal class. Inference associated with bj-abv (which is proved from fewer axioms). (Contributed by Stefan Allan, 9-Dec-2008)

	Ref	Expression
Hypothesis	sa-abvi.1	|- ph
Assertion	sa-abvi	|- _V = { x | ph }

Proof

Step	Hyp	Ref	Expression
1		sa-abvi.1	|- ph
2		df-v	|- _V = { x | x = x }
3		equid	|- x = x
4	3 1	2th	|- ( x = x <-> ph )
5	4	abbii	|- { x | x = x } = { x | ph }
6	2 5	eqtri	|- _V = { x | ph }