Theorem bj-restsnss

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

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

Proof

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