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	⊢ ( 𝐴 ∩ V ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		inss1	⊢ ( 𝐴 ∩ V ) ⊆ 𝐴
2		ssid	⊢ 𝐴 ⊆ 𝐴
3		ssv	⊢ 𝐴 ⊆ V
4	2 3	ssini	⊢ 𝐴 ⊆ ( 𝐴 ∩ V )
5	1 4	eqssi	⊢ ( 𝐴 ∩ V ) = 𝐴