This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem snres0

Description: Condition for restriction of a singleton to be empty. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypothesis snres0.1 ⊢ B ∈ V
Assertion snres0 ⊢ A B ↾ C = ∅ ↔ ¬ A ∈ C

Proof

Step Hyp Ref Expression
1 snres0.1 ⊢ B ∈ V
2 relres ⊢ Rel ⁡ A B ↾ C
3 reldm0 ⊢ Rel ⁡ A B ↾ C → A B ↾ C = ∅ ↔ dom ⁡ A B ↾ C = ∅
4 2 3 ax-mp ⊢ A B ↾ C = ∅ ↔ dom ⁡ A B ↾ C = ∅
5 dmres ⊢ dom ⁡ A B ↾ C = C ∩ dom ⁡ A B
6 1 dmsnop ⊢ dom ⁡ A B = A
7 6 ineq2i ⊢ C ∩ dom ⁡ A B = C ∩ A
8 5 7 eqtri ⊢ dom ⁡ A B ↾ C = C ∩ A
9 8 eqeq1i ⊢ dom ⁡ A B ↾ C = ∅ ↔ C ∩ A = ∅
10 disjsn ⊢ C ∩ A = ∅ ↔ ¬ A ∈ C
11 4 9 10 3bitri ⊢ A B ↾ C = ∅ ↔ ¬ A ∈ C