Theorem bj-restuni2

Description: The union of an elementwise intersection on a family of sets by a subset is equal to that subset. See also restuni and restuni2 . (Contributed by BJ, 27-Apr-2021)

	Ref	Expression
Assertion	bj-restuni2	|- ( ( X e. V /\ A C_ U. X ) -> U. ( X |`t A ) = A )

Proof

Step	Hyp	Ref	Expression
1		uniexg	|- ( X e. V -> U. X e. _V )
2		ssexg	|- ( ( A C_ U. X /\ U. X e. _V ) -> A e. _V )
3	1 2	sylan2	|- ( ( A C_ U. X /\ X e. V ) -> A e. _V )
4	3	ancoms	|- ( ( X e. V /\ A C_ U. X ) -> A e. _V )
5		bj-restuni	|- ( ( X e. V /\ A e. _V ) -> U. ( X |`t A ) = ( U. X i^i A ) )
6	4 5	syldan	|- ( ( X e. V /\ A C_ U. X ) -> U. ( X |`t A ) = ( U. X i^i A ) )
7		inss2	|- ( U. X i^i A ) C_ A
8	7	a1i	|- ( A C_ U. X -> ( U. X i^i A ) C_ A )
9		id	|- ( A C_ U. X -> A C_ U. X )
10		ssidd	|- ( A C_ U. X -> A C_ A )
11	9 10	ssind	|- ( A C_ U. X -> A C_ ( U. X i^i A ) )
12	8 11	eqssd	|- ( A C_ U. X -> ( U. X i^i A ) = A )
13	12	adantl	|- ( ( X e. V /\ A C_ U. X ) -> ( U. X i^i A ) = A )
14	6 13	eqtrd	|- ( ( X e. V /\ A C_ U. X ) -> U. ( X |`t A ) = A )