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 )