This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \cap V = A$

Proof

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