Theorem bj-restb

Description: An elementwise intersection by a set on a family containing a superset of that set contains that set. (Contributed by BJ, 27-Apr-2021)

	Ref	Expression
Assertion	bj-restb	|- ( X e. V -> ( ( A C_ B /\ B e. X ) -> A e. ( X |`t A ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( A C_ B -> A C_ B )
2		ssidd	|- ( A C_ B -> A C_ A )
3	1 2	ssind	|- ( A C_ B -> A C_ ( B i^i A ) )
4		inss2	|- ( B i^i A ) C_ A
5	4	a1i	|- ( A C_ B -> ( B i^i A ) C_ A )
6	3 5	eqssd	|- ( A C_ B -> A = ( B i^i A ) )
7		eleq1	|- ( y = B -> ( y e. X <-> B e. X ) )
8		ineq1	|- ( y = B -> ( y i^i A ) = ( B i^i A ) )
9	8	eqeq2d	|- ( y = B -> ( A = ( y i^i A ) <-> A = ( B i^i A ) ) )
10	7 9	anbi12d	|- ( y = B -> ( ( y e. X /\ A = ( y i^i A ) ) <-> ( B e. X /\ A = ( B i^i A ) ) ) )
11	10	spcegv	|- ( B e. X -> ( ( B e. X /\ A = ( B i^i A ) ) -> E. y ( y e. X /\ A = ( y i^i A ) ) ) )
12	11	expd	|- ( B e. X -> ( B e. X -> ( A = ( B i^i A ) -> E. y ( y e. X /\ A = ( y i^i A ) ) ) ) )
13	12	pm2.43i	|- ( B e. X -> ( A = ( B i^i A ) -> E. y ( y e. X /\ A = ( y i^i A ) ) ) )
14	6 13	mpan9	|- ( ( A C_ B /\ B e. X ) -> E. y ( y e. X /\ A = ( y i^i A ) ) )
15		df-rex	|- ( E. y e. X A = ( y i^i A ) <-> E. y ( y e. X /\ A = ( y i^i A ) ) )
16	14 15	sylibr	|- ( ( A C_ B /\ B e. X ) -> E. y e. X A = ( y i^i A ) )
17	16	adantl	|- ( ( X e. V /\ ( A C_ B /\ B e. X ) ) -> E. y e. X A = ( y i^i A ) )
18		ssexg	|- ( ( A C_ B /\ B e. X ) -> A e. _V )
19		elrest	|- ( ( X e. V /\ A e. _V ) -> ( A e. ( X |`t A ) <-> E. y e. X A = ( y i^i A ) ) )
20	18 19	sylan2	|- ( ( X e. V /\ ( A C_ B /\ B e. X ) ) -> ( A e. ( X |`t A ) <-> E. y e. X A = ( y i^i A ) ) )
21	17 20	mpbird	|- ( ( X e. V /\ ( A C_ B /\ B e. X ) ) -> A e. ( X |`t A ) )
22	21	ex	|- ( X e. V -> ( ( A C_ B /\ B e. X ) -> A e. ( X |`t A ) ) )