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

Metamath Proof Explorer

Theorem iunsn

Description: Indexed union of a singleton. Compare dfiun2 and rnmpt . (Contributed by Steven Nguyen, 7-Jun-2023)

Ref Expression
Assertion iunsn ⊢ ⋃ x ∈ A B = y | ∃ x ∈ A y = B

Proof

Step Hyp Ref Expression
1 df-iun ⊢ ⋃ x ∈ A B = y | ∃ x ∈ A y ∈ B
2 velsn ⊢ y ∈ B ↔ y = B
3 2 rexbii ⊢ ∃ x ∈ A y ∈ B ↔ ∃ x ∈ A y = B
4 3 abbii ⊢ y | ∃ x ∈ A y ∈ B = y | ∃ x ∈ A y = B
5 1 4 eqtri ⊢ ⋃ x ∈ A B = y | ∃ x ∈ A y = B