Metamath Proof Explorer


Theorem iunxsng

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

Ref Expression
Hypothesis iunxsng.1
|- ( x = A -> B = C )
Assertion iunxsng
|- ( A e. V -> U_ x e. { A } B = C )

Proof

Step Hyp Ref Expression
1 iunxsng.1
 |-  ( x = A -> B = C )
2 eliun
 |-  ( y e. U_ x e. { A } B <-> E. x e. { A } y e. B )
3 1 eleq2d
 |-  ( x = A -> ( y e. B <-> y e. C ) )
4 3 rexsng
 |-  ( A e. V -> ( E. x e. { A } y e. B <-> y e. C ) )
5 2 4 syl5bb
 |-  ( A e. V -> ( y e. U_ x e. { A } B <-> y e. C ) )
6 5 eqrdv
 |-  ( A e. V -> U_ x e. { A } B = C )