Theorem dmv

Description: The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003)

	Ref	Expression
Assertion	dmv	⊢ dom V = V

Proof

Step	Hyp	Ref	Expression
1		ssv	⊢ dom V ⊆ V
2		dmi	⊢ dom I = V
3		ssv	⊢ I ⊆ V
4		dmss	⊢ ( I ⊆ V → dom I ⊆ dom V )
5	3 4	ax-mp	⊢ dom I ⊆ dom V
6	2 5	eqsstrri	⊢ V ⊆ dom V
7	1 6	eqssi	⊢ dom V = V