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

Metamath Proof Explorer

Theorem iunxsnf

Description: A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses iunxsnf.1 ⊢ Ⅎ _ x C
iunxsnf.2 ⊢ A ∈ V
iunxsnf.3 ⊢ x = A → B = C
Assertion iunxsnf ⊢ ⋃ x ∈ A B = C

Proof

Step Hyp Ref Expression
1 iunxsnf.1 ⊢ Ⅎ _ x C
2 iunxsnf.2 ⊢ A ∈ V
3 iunxsnf.3 ⊢ x = A → B = C
4 1 3 iunxsngf ⊢ A ∈ V → ⋃ x ∈ A B = C
5 2 4 ax-mp ⊢ ⋃ x ∈ A B = C