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 ⊢ 𝐵 ∈ V
Assertion snres0 ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) = ∅ ↔ ¬ 𝐴 ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 snres0.1 ⊢ 𝐵 ∈ V
2 relres ⊢ Rel ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 )
3 reldm0 ⊢ ( Rel ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) → ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) = ∅ ↔ dom ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) = ∅ ) )
4 2 3 ax-mp ⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) = ∅ ↔ dom ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) = ∅ )
5 dmres ⊢ dom ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) = ( 𝐶 ∩ dom { ⟨ 𝐴 , 𝐵 ⟩ } )
6 1 dmsnop ⊢ dom { ⟨ 𝐴 , 𝐵 ⟩ } = { 𝐴 }
7 6 ineq2i ⊢ ( 𝐶 ∩ dom { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( 𝐶 ∩ { 𝐴 } )
8 5 7 eqtri ⊢ dom ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) = ( 𝐶 ∩ { 𝐴 } )
9 8 eqeq1i ⊢ ( dom ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) = ∅ ↔ ( 𝐶 ∩ { 𝐴 } ) = ∅ )
10 disjsn ⊢ ( ( 𝐶 ∩ { 𝐴 } ) = ∅ ↔ ¬ 𝐴 ∈ 𝐶 )
11 4 9 10 3bitri ⊢ ( ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) = ∅ ↔ ¬ 𝐴 ∈ 𝐶 )