Metamath Proof Explorer


Theorem iunsn

Description: Indexed union of a singleton. Compare dfiun2 and rnmpt . (Contributed by Steven Nguyen, 7-Jun-2023)

Ref Expression
Assertion iunsn x A B = y | x A y = B

Proof

Step Hyp Ref Expression
1 df-iun x A B = y | x A y B
2 velsn y B y = B
3 2 rexbii x A y B x A y = B
4 3 abbii y | x A y B = y | x A y = B
5 1 4 eqtri x A B = y | x A y = B