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