Metamath Proof Explorer


Theorem iunxsn

Description: A singleton index picks out an instance of an indexed union's argument. (Contributed by NM, 26-Mar-2004) (Proof shortened by Mario Carneiro, 25-Jun-2016)

Ref Expression
Hypotheses iunxsn.1
|- A e. _V
iunxsn.2
|- ( x = A -> B = C )
Assertion iunxsn
|- U_ x e. { A } B = C

Proof

Step Hyp Ref Expression
1 iunxsn.1
 |-  A e. _V
2 iunxsn.2
 |-  ( x = A -> B = C )
3 2 iunxsng
 |-  ( A e. _V -> U_ x e. { A } B = C )
4 1 3 ax-mp
 |-  U_ x e. { A } B = C