Metamath Proof Explorer

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 V = A


Step Hyp Ref Expression
1 inss1 A V A
2 ssid A A
3 ssv A V
4 2 3 ssini A A V
5 1 4 eqssi A V = A