Metamath Proof Explorer

Theorem elfpw

Description: Membership in a class of finite subsets. (Contributed by Stefan O'Rear, 4-Apr-2015) (Revised by Mario Carneiro, 22-Aug-2015)

		Ref	Expression
	Assertion	elfpw	$⊢ A \in (𝒫 B \cap Fin) \leftrightarrow (A \subseteq B \land A \in Fin)$

Step	Hyp	Ref	Expression
1		elin	$⊢ A \in (𝒫 B \cap Fin) \leftrightarrow (A \in 𝒫 B \land A \in Fin)$
2		elpwg	$⊢ A \in Fin \to (A \in 𝒫 B \leftrightarrow A \subseteq B)$
3	2	pm5.32ri	$⊢ (A \in 𝒫 B \land A \in Fin) \leftrightarrow (A \subseteq B \land A \in Fin)$
4	1 3	bitri	$⊢ A \in (𝒫 B \cap Fin) \leftrightarrow (A \subseteq B \land A \in Fin)$