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

Metamath Proof Explorer

Theorem ressnop0

Description: If A is not in C , then the restriction of a singleton of <. A , B >. to C is null. (Contributed by Scott Fenton, 15-Apr-2011)

Ref Expression
Assertion ressnop0 ( ¬ 𝐴 ∈ 𝐶 → ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) = ∅ )

Proof

Step Hyp Ref Expression
1 opelxp1 ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × V ) → 𝐴 ∈ 𝐶 )
2 df-res ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) = ( { ⟨ 𝐴 , 𝐵 ⟩ } ∩ ( 𝐶 × V ) )
3 incom ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } ∩ ( 𝐶 × V ) ) = ( ( 𝐶 × V ) ∩ { ⟨ 𝐴 , 𝐵 ⟩ } )
4 2 3 eqtri ⊢ ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) = ( ( 𝐶 × V ) ∩ { ⟨ 𝐴 , 𝐵 ⟩ } )
5 disjsn ⊢ ( ( ( 𝐶 × V ) ∩ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ∅ ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × V ) )
6 5 biimpri ⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × V ) → ( ( 𝐶 × V ) ∩ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ∅ )
7 4 6 eqtrid ⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × V ) → ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) = ∅ )
8 1 7 nsyl5 ⊢ ( ¬ 𝐴 ∈ 𝐶 → ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) = ∅ )