Step |
Hyp |
Ref |
Expression |
1 |
|
df-eprel |
|- _E = { <. x , y >. | x e. y } |
2 |
|
df-id |
|- _I = { <. x , y >. | x = y } |
3 |
1 2
|
ineq12i |
|- ( _E i^i _I ) = ( { <. x , y >. | x e. y } i^i { <. x , y >. | x = y } ) |
4 |
|
inopab |
|- ( { <. x , y >. | x e. y } i^i { <. x , y >. | x = y } ) = { <. x , y >. | ( x e. y /\ x = y ) } |
5 |
|
nelaneq |
|- -. ( x e. y /\ x = y ) |
6 |
5
|
gen2 |
|- A. x A. y -. ( x e. y /\ x = y ) |
7 |
|
opab0 |
|- ( { <. x , y >. | ( x e. y /\ x = y ) } = (/) <-> A. x A. y -. ( x e. y /\ x = y ) ) |
8 |
6 7
|
mpbir |
|- { <. x , y >. | ( x e. y /\ x = y ) } = (/) |
9 |
3 4 8
|
3eqtri |
|- ( _E i^i _I ) = (/) |