Metamath Proof Explorer


Theorem bj-restsnss2

Description: Special case of bj-restsn . (Contributed by BJ, 27-Apr-2021)

Ref Expression
Assertion bj-restsnss2
|- ( ( A e. V /\ Y C_ A ) -> ( { Y } |`t A ) = { Y } )

Proof

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 } )