Step |
Hyp |
Ref |
Expression |
1 |
|
df-ss |
|- ( Y C_ A <-> ( Y i^i A ) = Y ) |
2 |
|
sneq |
|- ( ( Y i^i A ) = Y -> { ( Y i^i A ) } = { Y } ) |
3 |
1 2
|
sylbi |
|- ( Y C_ A -> { ( Y i^i A ) } = { Y } ) |
4 |
|
ssexg |
|- ( ( Y C_ A /\ A e. V ) -> Y e. _V ) |
5 |
4
|
ancoms |
|- ( ( A e. V /\ Y C_ A ) -> Y e. _V ) |
6 |
|
bj-restsn |
|- ( ( Y e. _V /\ A e. V ) -> ( { Y } |`t A ) = { ( Y i^i A ) } ) |
7 |
6
|
ancoms |
|- ( ( A e. V /\ Y e. _V ) -> ( { Y } |`t A ) = { ( Y i^i A ) } ) |
8 |
5 7
|
syldan |
|- ( ( A e. V /\ Y C_ A ) -> ( { Y } |`t A ) = { ( Y i^i A ) } ) |
9 |
|
eqeq2 |
|- ( { ( Y i^i A ) } = { Y } -> ( ( { Y } |`t A ) = { ( Y i^i A ) } <-> ( { Y } |`t A ) = { Y } ) ) |
10 |
9
|
biimpa |
|- ( ( { ( Y i^i A ) } = { Y } /\ ( { Y } |`t A ) = { ( Y i^i A ) } ) -> ( { Y } |`t A ) = { Y } ) |
11 |
3 8 10
|
syl2an2 |
|- ( ( A e. V /\ Y C_ A ) -> ( { Y } |`t A ) = { Y } ) |