Metamath Proof Explorer


Theorem djussxp2

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

Ref Expression
Assertion djussxp2 k A k × B A × k A B

Proof

Step Hyp Ref Expression
1 nfcv _ k A
2 nfiu1 _ k k A B
3 1 2 nfxp _ k A × k A B
4 3 iunssf k A k × B A × k A B k A k × B A × k A B
5 snssi k A k A
6 ssiun2 k A B k A B
7 xpss12 k A B k A B k × B A × k A B
8 5 6 7 syl2anc k A k × B A × k A B
9 4 8 mprgbir k A k × B A × k A B