Metamath Proof Explorer

Theorem bj-rest10

Description: An elementwise intersection on a nonempty family by the empty set is the singleton on the empty set. TODO: this generalizes rest0 and could replace it. (Contributed by BJ, 27-Apr-2021)

Ref Expression
Assertion bj-rest10 ⊢ X ∈ V → X ≠ ∅ → X ↾ 𝑡 ∅ = ∅

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 elrest ⊢ X ∈ V ∧ ∅ ∈ V → x ∈ X ↾ 𝑡 ∅ ↔ ∃ y ∈ X x = y ∩ ∅
3 1 2 mpan2 ⊢ X ∈ V → x ∈ X ↾ 𝑡 ∅ ↔ ∃ y ∈ X x = y ∩ ∅
4 in0 ⊢ y ∩ ∅ = ∅
5 4 eqeq2i ⊢ x = y ∩ ∅ ↔ x = ∅
6 5 rexbii ⊢ ∃ y ∈ X x = y ∩ ∅ ↔ ∃ y ∈ X x = ∅
7 df-rex ⊢ ∃ y ∈ X x = ∅ ↔ ∃ y y ∈ X ∧ x = ∅
8 19.41v ⊢ ∃ y y ∈ X ∧ x = ∅ ↔ ∃ y y ∈ X ∧ x = ∅
9 n0 ⊢ X ≠ ∅ ↔ ∃ y y ∈ X
10 9 bicomi ⊢ ∃ y y ∈ X ↔ X ≠ ∅
11 10 anbi1i ⊢ ∃ y y ∈ X ∧ x = ∅ ↔ X ≠ ∅ ∧ x = ∅
12 8 11 bitri ⊢ ∃ y y ∈ X ∧ x = ∅ ↔ X ≠ ∅ ∧ x = ∅
13 7 12 bitri ⊢ ∃ y ∈ X x = ∅ ↔ X ≠ ∅ ∧ x = ∅
14 6 13 bitri ⊢ ∃ y ∈ X x = y ∩ ∅ ↔ X ≠ ∅ ∧ x = ∅
15 14 baib ⊢ X ≠ ∅ → ∃ y ∈ X x = y ∩ ∅ ↔ x = ∅
16 3 15 sylan9bb ⊢ X ∈ V ∧ X ≠ ∅ → x ∈ X ↾ 𝑡 ∅ ↔ x = ∅
17 velsn ⊢ x ∈ ∅ ↔ x = ∅
18 16 17 bitr4di ⊢ X ∈ V ∧ X ≠ ∅ → x ∈ X ↾ 𝑡 ∅ ↔ x ∈ ∅
19 18 eqrdv ⊢ X ∈ V ∧ X ≠ ∅ → X ↾ 𝑡 ∅ = ∅
20 19 ex ⊢ X ∈ V → X ≠ ∅ → X ↾ 𝑡 ∅ = ∅