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 ) ) ) |
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 ) ) ) |