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 i^i _V ) = A

Proof

Step	Hyp	Ref	Expression
1		inss1	|- ( A i^i _V ) C_ A
2		ssid	|- A C_ A
3		ssv	|- A C_ _V
4	2 3	ssini	|- A C_ ( A i^i _V )
5	1 4	eqssi	|- ( A i^i _V ) = A