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	⊢ 𝜑
Assertion	sa-abvi	⊢ V = { 𝑥 ∣ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		sa-abvi.1	⊢ 𝜑
2		df-v	⊢ V = { 𝑥 ∣ 𝑥 = 𝑥 }
3		equid	⊢ 𝑥 = 𝑥
4	3 1	2th	⊢ ( 𝑥 = 𝑥 ↔ 𝜑 )
5	4	abbii	⊢ { 𝑥 ∣ 𝑥 = 𝑥 } = { 𝑥 ∣ 𝜑 }
6	2 5	eqtri	⊢ V = { 𝑥 ∣ 𝜑 }