Metamath Proof Explorer

Theorem bj-rest0

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

Ref Expression
Assertion bj-rest0 ⊢ X ∈ V ∧ A ∈ W → ∅ ∈ X → ∅ ∈ X ↾ 𝑡 A

Proof

Step Hyp Ref Expression
1 in0 ⊢ A ∩ ∅ = ∅
2 incom ⊢ A ∩ ∅ = ∅ ∩ A
3 1 2 eqtr3i ⊢ ∅ = ∅ ∩ A
4 0ex ⊢ ∅ ∈ V
5 eleq1 ⊢ x = ∅ → x ∈ X ↔ ∅ ∈ X
6 ineq1 ⊢ x = ∅ → x ∩ A = ∅ ∩ A
7 6 eqeq2d ⊢ x = ∅ → ∅ = x ∩ A ↔ ∅ = ∅ ∩ A
8 5 7 anbi12d ⊢ x = ∅ → x ∈ X ∧ ∅ = x ∩ A ↔ ∅ ∈ X ∧ ∅ = ∅ ∩ A
9 4 8 spcev ⊢ ∅ ∈ X ∧ ∅ = ∅ ∩ A → ∃ x x ∈ X ∧ ∅ = x ∩ A
10 3 9 mpan2 ⊢ ∅ ∈ X → ∃ x x ∈ X ∧ ∅ = x ∩ A
11 df-rex ⊢ ∃ x ∈ X ∅ = x ∩ A ↔ ∃ x x ∈ X ∧ ∅ = x ∩ A
12 10 11 sylibr ⊢ ∅ ∈ X → ∃ x ∈ X ∅ = x ∩ A
13 elrest ⊢ X ∈ V ∧ A ∈ W → ∅ ∈ X ↾ 𝑡 A ↔ ∃ x ∈ X ∅ = x ∩ A
14 12 13 imbitrrid ⊢ X ∈ V ∧ A ∈ W → ∅ ∈ X → ∅ ∈ X ↾ 𝑡 A