Metamath Proof Explorer


Theorem ssuni

Description: Subclass relationship for class union. (Contributed by NM, 24-May-1994) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Proof shortened by JJ, 26-Jul-2021)

Ref Expression
Assertion ssuni ( ( 𝐴𝐵𝐵𝐶 ) → 𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 elunii ( ( 𝑥𝐵𝐵𝐶 ) → 𝑥 𝐶 )
2 1 expcom ( 𝐵𝐶 → ( 𝑥𝐵𝑥 𝐶 ) )
3 2 imim2d ( 𝐵𝐶 → ( ( 𝑥𝐴𝑥𝐵 ) → ( 𝑥𝐴𝑥 𝐶 ) ) )
4 3 alimdv ( 𝐵𝐶 → ( ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) → ∀ 𝑥 ( 𝑥𝐴𝑥 𝐶 ) ) )
5 dfss2 ( 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) )
6 dfss2 ( 𝐴 𝐶 ↔ ∀ 𝑥 ( 𝑥𝐴𝑥 𝐶 ) )
7 4 5 6 3imtr4g ( 𝐵𝐶 → ( 𝐴𝐵𝐴 𝐶 ) )
8 7 impcom ( ( 𝐴𝐵𝐵𝐶 ) → 𝐴 𝐶 )