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

Metamath Proof Explorer

Theorem chm1i

Description: Meet with lattice one in CH . (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	ch0le.1	$⊢ A \in C_{ℋ}$
	Assertion	chm1i	$⊢ A \cap ℋ = A$

Step	Hyp	Ref	Expression
1		ch0le.1	$⊢ A \in C_{ℋ}$
2	1	chssii	$⊢ A \subseteq ℋ$
3		dfss2	$⊢ A \subseteq ℋ \leftrightarrow A \cap ℋ = A$
4	2 3	mpbi	$⊢ A \cap ℋ = A$