| Step |
Hyp |
Ref |
Expression |
| 1 |
|
equvinv |
|- ( y = z <-> E. x ( x = y /\ x = z ) ) |
| 2 |
|
ideqg |
|- ( y e. _V -> ( x _I y <-> x = y ) ) |
| 3 |
2
|
elv |
|- ( x _I y <-> x = y ) |
| 4 |
|
ideqg |
|- ( z e. _V -> ( x _I z <-> x = z ) ) |
| 5 |
4
|
elv |
|- ( x _I z <-> x = z ) |
| 6 |
3 5
|
anbi12i |
|- ( ( x _I y /\ x _I z ) <-> ( x = y /\ x = z ) ) |
| 7 |
6
|
exbii |
|- ( E. x ( x _I y /\ x _I z ) <-> E. x ( x = y /\ x = z ) ) |
| 8 |
1 7
|
bitr4i |
|- ( y = z <-> E. x ( x _I y /\ x _I z ) ) |
| 9 |
8
|
opabbii |
|- { <. y , z >. | y = z } = { <. y , z >. | E. x ( x _I y /\ x _I z ) } |
| 10 |
|
df-id |
|- _I = { <. y , z >. | y = z } |
| 11 |
|
df-coss |
|- ,~ _I = { <. y , z >. | E. x ( x _I y /\ x _I z ) } |
| 12 |
9 10 11
|
3eqtr4ri |
|- ,~ _I = _I |