Metamath Proof Explorer


Theorem bj-restsn

Description: An elementwise intersection on the singleton on a set is the singleton on the intersection by that set. Generalization of bj-restsn0 and bj-restsnid . (Contributed by BJ, 27-Apr-2021)

Ref Expression
Assertion bj-restsn Y V A W Y 𝑡 A = Y A

Proof

Step Hyp Ref Expression
1 snex Y V
2 elrest Y V A W x Y 𝑡 A y Y x = y A
3 1 2 mpan A W x Y 𝑡 A y Y x = y A
4 velsn x y A x = y A
5 ineq1 y = Y y A = Y A
6 5 sneqd y = Y y A = Y A
7 6 eleq2d y = Y x y A x Y A
8 4 7 bitr3id y = Y x = y A x Y A
9 8 rexsng Y V y Y x = y A x Y A
10 3 9 sylan9bbr Y V A W x Y 𝑡 A x Y A
11 10 eqrdv Y V A W Y 𝑡 A = Y A