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 _xC
iunxsnf.2 AV
iunxsnf.3 x=AB=C
Assertion iunxsnf xAB=C

Proof

Step Hyp Ref Expression
1 iunxsnf.1 _xC
2 iunxsnf.2 AV
3 iunxsnf.3 x=AB=C
4 1 3 iunxsngf AVxAB=C
5 2 4 ax-mp xAB=C