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	$$⊢\phi$$
Assertion	sa-abvi	$$⊢\mathrm{V}=\left\{x|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		sa-abvi.1	$$⊢\phi$$
2		df-v	$$⊢\mathrm{V}=\left\{x|x=x\right\}$$
3		equid	$$⊢x=x$$
4	3 1	2th	$$⊢x=x\leftrightarrow \phi$$
5	4	abbii	$$⊢\left\{x|x=x\right\}=\left\{x|\phi \right\}$$
6	2 5	eqtri	$$⊢\mathrm{V}=\left\{x|\phi \right\}$$