Step |
Hyp |
Ref |
Expression |
1 |
|
df-tr |
|- ( Tr A <-> U. A C_ A ) |
2 |
|
ssralv |
|- ( U. A C_ A -> ( A. x e. A -. x e. x -> A. x e. U. A -. x e. x ) ) |
3 |
1 2
|
sylbi |
|- ( Tr A -> ( A. x e. A -. x e. x -> A. x e. U. A -. x e. x ) ) |
4 |
|
elequ1 |
|- ( x = y -> ( x e. x <-> y e. x ) ) |
5 |
|
elequ2 |
|- ( x = y -> ( y e. x <-> y e. y ) ) |
6 |
4 5
|
bitrd |
|- ( x = y -> ( x e. x <-> y e. y ) ) |
7 |
6
|
notbid |
|- ( x = y -> ( -. x e. x <-> -. y e. y ) ) |
8 |
7
|
cbvralvw |
|- ( A. x e. U. A -. x e. x <-> A. y e. U. A -. y e. y ) |
9 |
|
untuni |
|- ( A. y e. U. A -. y e. y <-> A. x e. A A. y e. x -. y e. y ) |
10 |
8 9
|
bitri |
|- ( A. x e. U. A -. x e. x <-> A. x e. A A. y e. x -. y e. y ) |
11 |
3 10
|
syl6ib |
|- ( Tr A -> ( A. x e. A -. x e. x -> A. x e. A A. y e. x -. y e. y ) ) |
12 |
|
untelirr |
|- ( A. y e. x -. y e. y -> -. x e. x ) |
13 |
12
|
ralimi |
|- ( A. x e. A A. y e. x -. y e. y -> A. x e. A -. x e. x ) |
14 |
11 13
|
impbid1 |
|- ( Tr A -> ( A. x e. A -. x e. x <-> A. x e. A A. y e. x -. y e. y ) ) |