Metamath Proof Explorer


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 X X X A X 𝑡 A

Proof

Step Hyp Ref Expression
1 uniexr X X X V
2 1 adantl A X X X X V
3 bj-restb X V A X X X A X 𝑡 A
4 2 3 mpcom A X X X A X 𝑡 A