elfi

Description: Specific properties of an element of ( fiB ) . (Contributed by FL, 27-Apr-2008) (Revised by Mario Carneiro, 24-Nov-2013)

		Ref	Expression
	Assertion	elfi	$⊢ (A \in V \land B \in W) \to (A \in fi (B) \leftrightarrow \exists x \in (𝒫 B \cap Fin) A = ⋂ x)$

Step	Hyp	Ref	Expression
1		fival	$⊢ B \in W \to fi (B) = \{y \| \exists x \in (𝒫 B \cap Fin) y = ⋂ x\}$
2	1	eleq2d	$⊢ B \in W \to (A \in fi (B) \leftrightarrow A \in \{y \| \exists x \in (𝒫 B \cap Fin) y = ⋂ x\})$
3		eqeq1	$⊢ y = A \to (y = ⋂ x \leftrightarrow A = ⋂ x)$
4	3	rexbidv	$⊢ y = A \to (\exists x \in (𝒫 B \cap Fin) y = ⋂ x \leftrightarrow \exists x \in (𝒫 B \cap Fin) A = ⋂ x)$
5	4	elabg	$⊢ A \in V \to (A \in \{y \| \exists x \in (𝒫 B \cap Fin) y = ⋂ x\} \leftrightarrow \exists x \in (𝒫 B \cap Fin) A = ⋂ x)$
6	2 5	sylan9bbr	$⊢ (A \in V \land B \in W) \to (A \in fi (B) \leftrightarrow \exists x \in (𝒫 B \cap Fin) A = ⋂ x)$

Metamath Proof Explorer