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 ⊢ Ⅎ 𝑥 𝐶
iunxsnf.2 ⊢ 𝐴 ∈ V
iunxsnf.3 ⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
Assertion iunxsnf ∪ 𝑥 ∈ { 𝐴 } 𝐵 = 𝐶

Proof

Step Hyp Ref Expression
1 iunxsnf.1 ⊢ Ⅎ 𝑥 𝐶
2 iunxsnf.2 ⊢ 𝐴 ∈ V
3 iunxsnf.3 ⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
4 1 3 iunxsngf ⊢ ( 𝐴 ∈ V → ∪ 𝑥 ∈ { 𝐴 } 𝐵 = 𝐶 )
5 2 4 ax-mp ⊢ ∪ 𝑥 ∈ { 𝐴 } 𝐵 = 𝐶