Theorem inv1

Description: The intersection of a class with the universal class is itself. Exercise 4.10(k) of Mendelson p. 231. (Contributed by NM, 17-May-1998)

	Ref	Expression
Assertion	inv1	$$⊢A\cap \mathrm{V}=A$$

Proof

Step	Hyp	Ref	Expression
1		inss1	$$⊢A\cap \mathrm{V}\subseteq A$$
2		ssid	$$⊢A\subseteq A$$
3		ssv	$$⊢A\subseteq \mathrm{V}$$
4	2 3	ssini	$$⊢A\subseteq A\cap \mathrm{V}$$
5	1 4	eqssi	$$⊢A\cap \mathrm{V}=A$$