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