Metamath Proof Explorer


Theorem expanduniss

Description: Expand U. A C_ B to primitives. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Assertion expanduniss A B x x A y y x y B

Proof

Step Hyp Ref Expression
1 unissb A B x A x B
2 dfss2 x B y y x y B
3 2 expandral x A x B x x A y y x y B
4 1 3 bitri A B x x A y y x y B