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 𝑥 ∈ { 𝐴 } 𝐵 = 𝐶