Metamath Proof Explorer


Theorem ssiun2

Description: Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion ssiun2 xABxAB

Proof

Step Hyp Ref Expression
1 rspe xAyBxAyB
2 1 ex xAyBxAyB
3 eliun yxABxAyB
4 2 3 imbitrrdi xAyByxAB
5 4 ssrdv xABxAB