Metamath Proof Explorer

Theorem bj-resta

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

Ref Expression
Assertion bj-resta 
|- ( X e. V -> ( A e. X -> A e. ( X |`t A ) ) )

Proof

Step Hyp Ref Expression
1 ssid 
 |-  A C_ A
2 bj-restb 
 |-  ( X e. V -> ( ( A C_ A /\ A e. X ) -> A e. ( X |`t A ) ) )
3 1 2 mpani 
 |-  ( X e. V -> ( A e. X -> A e. ( X |`t A ) ) )