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