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	syl5eq	⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝐶 × V ) → ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) = ∅ )
8	1 7	nsyl5	⊢ ( ¬ 𝐴 ∈ 𝐶 → ( { ⟨ 𝐴 , 𝐵 ⟩ } ↾ 𝐶 ) = ∅ )