Step |
Hyp |
Ref |
Expression |
1 |
|
gruex |
|- E. y e. Univ x e. y |
2 |
1
|
ax-gen |
|- A. x E. y e. Univ x e. y |
3 |
|
rr-grothprimbi |
|- ( A. x E. y e. Univ x e. y <-> A. x -. A. y ( x e. y -> -. A. z ( z e. y -> A. f -. A. w ( w e. y -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. y -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. y -> ( i e. v -> ( v e. f -> -. A. u ( u e. f -> ( i e. u -> -. A. o ( o e. u -> A. s ( s e. o -> s e. w ) ) ) ) ) ) ) ) ) ) ) ) ) |
4 |
2 3
|
mpbi |
|- A. x -. A. y ( x e. y -> -. A. z ( z e. y -> A. f -. A. w ( w e. y -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. y -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. y -> ( i e. v -> ( v e. f -> -. A. u ( u e. f -> ( i e. u -> -. A. o ( o e. u -> A. s ( s e. o -> s e. w ) ) ) ) ) ) ) ) ) ) ) ) |
5 |
4
|
spi |
|- -. A. y ( x e. y -> -. A. z ( z e. y -> A. f -. A. w ( w e. y -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. y -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. y -> ( i e. v -> ( v e. f -> -. A. u ( u e. f -> ( i e. u -> -. A. o ( o e. u -> A. s ( s e. o -> s e. w ) ) ) ) ) ) ) ) ) ) ) ) |