Metamath Proof Explorer


Theorem expanduniss

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

Ref Expression
Assertion expanduniss
|- ( U. A C_ B <-> A. x ( x e. A -> A. y ( y e. x -> y e. B ) ) )

Proof

Step Hyp Ref Expression
1 unissb
 |-  ( U. A C_ B <-> A. x e. A x C_ B )
2 dfss2
 |-  ( x C_ B <-> A. y ( y e. x -> y e. B ) )
3 2 expandral
 |-  ( A. x e. A x C_ B <-> A. x ( x e. A -> A. y ( y e. x -> y e. B ) ) )
4 1 3 bitri
 |-  ( U. A C_ B <-> A. x ( x e. A -> A. y ( y e. x -> y e. B ) ) )