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