Metamath Proof Explorer

Theorem 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 ∈ V ∧ B ∈ W → A ∈ fi ⁡ B ↔ ∃ x ∈ 𝒫 B ∩ Fin A = ⋂ x

Proof

Step Hyp Ref Expression
1 fival ⊢ B ∈ W → fi ⁡ B = y | ∃ x ∈ 𝒫 B ∩ Fin y = ⋂ x
2 1 eleq2d ⊢ B ∈ W → A ∈ fi ⁡ B ↔ A ∈ y | ∃ x ∈ 𝒫 B ∩ Fin y = ⋂ x
3 eqeq1 ⊢ y = A → y = ⋂ x ↔ A = ⋂ x
4 3 rexbidv ⊢ y = A → ∃ x ∈ 𝒫 B ∩ Fin y = ⋂ x ↔ ∃ x ∈ 𝒫 B ∩ Fin A = ⋂ x
5 4 elabg ⊢ A ∈ V → A ∈ y | ∃ x ∈ 𝒫 B ∩ Fin y = ⋂ x ↔ ∃ x ∈ 𝒫 B ∩ Fin A = ⋂ x
6 2 5 sylan9bbr ⊢ A ∈ V ∧ B ∈ W → A ∈ fi ⁡ B ↔ ∃ x ∈ 𝒫 B ∩ Fin A = ⋂ x