Metamath Proof Explorer

Theorem intimasn

Description: Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020)

Ref Expression
Assertion intimasn ⊢ B ∈ V → ⋂ A B = ⋂ x | ∃ a ∈ A x = a B

Proof

Step Hyp Ref Expression
1 ax-5 ⊢ B ∈ V → ∀ y B ∈ V
2 r19.12sn ⊢ B ∈ V → ∃ b ∈ B ∀ a ∈ A b y ∈ a ↔ ∀ a ∈ A ∃ b ∈ B b y ∈ a
3 2 biimprd ⊢ B ∈ V → ∀ a ∈ A ∃ b ∈ B b y ∈ a → ∃ b ∈ B ∀ a ∈ A b y ∈ a
4 3 alimi ⊢ ∀ y B ∈ V → ∀ y ∀ a ∈ A ∃ b ∈ B b y ∈ a → ∃ b ∈ B ∀ a ∈ A b y ∈ a
5 intimag ⊢ ∀ y ∀ a ∈ A ∃ b ∈ B b y ∈ a → ∃ b ∈ B ∀ a ∈ A b y ∈ a → ⋂ A B = ⋂ x | ∃ a ∈ A x = a B
6 1 4 5 3syl ⊢ B ∈ V → ⋂ A B = ⋂ x | ∃ a ∈ A x = a B