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 ( 𝑋𝑉 → ( ( 𝐴𝐵𝐵𝑋 ) → 𝐴 ∈ ( 𝑋t 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 id ( 𝐴𝐵𝐴𝐵 )
2 ssidd ( 𝐴𝐵𝐴𝐴 )
3 1 2 ssind ( 𝐴𝐵𝐴 ⊆ ( 𝐵𝐴 ) )
4 inss2 ( 𝐵𝐴 ) ⊆ 𝐴
5 4 a1i ( 𝐴𝐵 → ( 𝐵𝐴 ) ⊆ 𝐴 )
6 3 5 eqssd ( 𝐴𝐵𝐴 = ( 𝐵𝐴 ) )
7 eleq1 ( 𝑦 = 𝐵 → ( 𝑦𝑋𝐵𝑋 ) )
8 ineq1 ( 𝑦 = 𝐵 → ( 𝑦𝐴 ) = ( 𝐵𝐴 ) )
9 8 eqeq2d ( 𝑦 = 𝐵 → ( 𝐴 = ( 𝑦𝐴 ) ↔ 𝐴 = ( 𝐵𝐴 ) ) )
10 7 9 anbi12d ( 𝑦 = 𝐵 → ( ( 𝑦𝑋𝐴 = ( 𝑦𝐴 ) ) ↔ ( 𝐵𝑋𝐴 = ( 𝐵𝐴 ) ) ) )
11 10 spcegv ( 𝐵𝑋 → ( ( 𝐵𝑋𝐴 = ( 𝐵𝐴 ) ) → ∃ 𝑦 ( 𝑦𝑋𝐴 = ( 𝑦𝐴 ) ) ) )
12 11 expd ( 𝐵𝑋 → ( 𝐵𝑋 → ( 𝐴 = ( 𝐵𝐴 ) → ∃ 𝑦 ( 𝑦𝑋𝐴 = ( 𝑦𝐴 ) ) ) ) )
13 12 pm2.43i ( 𝐵𝑋 → ( 𝐴 = ( 𝐵𝐴 ) → ∃ 𝑦 ( 𝑦𝑋𝐴 = ( 𝑦𝐴 ) ) ) )
14 6 13 mpan9 ( ( 𝐴𝐵𝐵𝑋 ) → ∃ 𝑦 ( 𝑦𝑋𝐴 = ( 𝑦𝐴 ) ) )
15 df-rex ( ∃ 𝑦𝑋 𝐴 = ( 𝑦𝐴 ) ↔ ∃ 𝑦 ( 𝑦𝑋𝐴 = ( 𝑦𝐴 ) ) )
16 14 15 sylibr ( ( 𝐴𝐵𝐵𝑋 ) → ∃ 𝑦𝑋 𝐴 = ( 𝑦𝐴 ) )
17 16 adantl ( ( 𝑋𝑉 ∧ ( 𝐴𝐵𝐵𝑋 ) ) → ∃ 𝑦𝑋 𝐴 = ( 𝑦𝐴 ) )
18 ssexg ( ( 𝐴𝐵𝐵𝑋 ) → 𝐴 ∈ V )
19 elrest ( ( 𝑋𝑉𝐴 ∈ V ) → ( 𝐴 ∈ ( 𝑋t 𝐴 ) ↔ ∃ 𝑦𝑋 𝐴 = ( 𝑦𝐴 ) ) )
20 18 19 sylan2 ( ( 𝑋𝑉 ∧ ( 𝐴𝐵𝐵𝑋 ) ) → ( 𝐴 ∈ ( 𝑋t 𝐴 ) ↔ ∃ 𝑦𝑋 𝐴 = ( 𝑦𝐴 ) ) )
21 17 20 mpbird ( ( 𝑋𝑉 ∧ ( 𝐴𝐵𝐵𝑋 ) ) → 𝐴 ∈ ( 𝑋t 𝐴 ) )
22 21 ex ( 𝑋𝑉 → ( ( 𝐴𝐵𝐵𝑋 ) → 𝐴 ∈ ( 𝑋t 𝐴 ) ) )