This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )