| Step |
Hyp |
Ref |
Expression |
| 1 |
|
rabab |
|- { x e. _V | ( card ` x ) = x } = { x | ( card ` x ) = x } |
| 2 |
|
fveq2 |
|- ( x = y -> ( card ` x ) = ( card ` y ) ) |
| 3 |
|
id |
|- ( x = y -> x = y ) |
| 4 |
2 3
|
eqeq12d |
|- ( x = y -> ( ( card ` x ) = x <-> ( card ` y ) = y ) ) |
| 5 |
4
|
cbvrabv |
|- { x e. _V | ( card ` x ) = x } = { y e. _V | ( card ` y ) = y } |
| 6 |
1 5
|
eqtr3i |
|- { x | ( card ` x ) = x } = { y e. _V | ( card ` y ) = y } |
| 7 |
|
fvexd |
|- ( { x | ( card ` x ) = x } e. _V -> ( har ` U. { x | ( card ` x ) = x } ) e. _V ) |
| 8 |
6 7
|
cardprcr |
|- -. { x | ( card ` x ) = x } e. _V |
| 9 |
8
|
nelir |
|- { x | ( card ` x ) = x } e/ _V |