Theorem bj-restv

Description: An elementwise intersection by a subset on a family containing the whole set contains the whole subset. (Contributed by BJ, 27-Apr-2021)

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

Proof

Step	Hyp	Ref	Expression
1		uniexr	|- ( U. X e. X -> X e. _V )
2	1	adantl	|- ( ( A C_ U. X /\ U. X e. X ) -> X e. _V )
3		bj-restb	|- ( X e. _V -> ( ( A C_ U. X /\ U. X e. X ) -> A e. ( X |`t A ) ) )
4	2 3	mpcom	|- ( ( A C_ U. X /\ U. X e. X ) -> A e. ( X |`t A ) )