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∈Xx=y∩∅
3 1 2 mpan2 ⊢X∈V→x∈X↾𝑡∅↔∃y∈Xx=y∩∅
4 in0 ⊢y∩∅=∅
5 4 eqeq2i ⊢x=y∩∅↔x=∅
6 5 rexbii ⊢∃y∈Xx=y∩∅↔∃y∈Xx=∅
7 df-rex ⊢∃y∈Xx=∅↔∃yy∈X∧x=∅
8 19.41v ⊢∃yy∈X∧x=∅↔∃yy∈X∧x=∅
9 n0 ⊢X≠∅↔∃yy∈X
10 9 bicomi ⊢∃yy∈X↔X≠∅
11 10 anbi1i ⊢∃yy∈X∧x=∅↔X≠∅∧x=∅
12 8 11 bitri ⊢∃yy∈X∧x=∅↔X≠∅∧x=∅
13 7 12 bitri ⊢∃y∈Xx=∅↔X≠∅∧x=∅
14 6 13 bitri ⊢∃y∈Xx=y∩∅↔X≠∅∧x=∅
15 14 baib ⊢X≠∅→∃y∈Xx=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↾𝑡∅=∅