Metamath Proof Explorer


Theorem djussxp2

Description: Stronger version of djussxp . (Contributed by Thierry Arnoux, 23-Jun-2024)

Ref Expression
Assertion djussxp2
|- U_ k e. A ( { k } X. B ) C_ ( A X. U_ k e. A B )

Proof

Step Hyp Ref Expression
1 nfcv
 |-  F/_ k A
2 nfiu1
 |-  F/_ k U_ k e. A B
3 1 2 nfxp
 |-  F/_ k ( A X. U_ k e. A B )
4 3 iunssf
 |-  ( U_ k e. A ( { k } X. B ) C_ ( A X. U_ k e. A B ) <-> A. k e. A ( { k } X. B ) C_ ( A X. U_ k e. A B ) )
5 snssi
 |-  ( k e. A -> { k } C_ A )
6 ssiun2
 |-  ( k e. A -> B C_ U_ k e. A B )
7 xpss12
 |-  ( ( { k } C_ A /\ B C_ U_ k e. A B ) -> ( { k } X. B ) C_ ( A X. U_ k e. A B ) )
8 5 6 7 syl2anc
 |-  ( k e. A -> ( { k } X. B ) C_ ( A X. U_ k e. A B ) )
9 4 8 mprgbir
 |-  U_ k e. A ( { k } X. B ) C_ ( A X. U_ k e. A B )