Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 id A B A B
2 ssidd A B A A
3 1 2 ssind A B A B A
4 inss2 B A A
5 4 a1i A B B A A
6 3 5 eqssd A B A = B A
7 eleq1 y = B y X B X
8 ineq1 y = B y A = B A
9 8 eqeq2d y = B A = y A A = B A
10 7 9 anbi12d y = B y X A = y A B X A = B A
11 10 spcegv B X B X A = B A y y X A = y A
12 11 expd B X B X A = B A y y X A = y A
13 12 pm2.43i B X A = B A y y X A = y A
14 6 13 mpan9 A B B X y y X A = y A
15 df-rex y X A = y A y y X A = y A
16 14 15 sylibr A B B X y X A = y A
17 16 adantl X V A B B X y X A = y A
18 ssexg A B B X A V
19 elrest X V A V A X 𝑡 A y X A = y A
20 18 19 sylan2 X V A B B X A X 𝑡 A y X A = y A
21 17 20 mpbird X V A B B X A X 𝑡 A
22 21 ex X V A B B X A X 𝑡 A