Metamath Proof Explorer


Theorem fnresdisj

Description: A function restricted to a class disjoint with its domain is empty. (Contributed by NM, 23-Sep-2004)

Ref Expression
Assertion fnresdisj F Fn A A B = F B =

Proof

Step Hyp Ref Expression
1 relres Rel F B
2 reldm0 Rel F B F B = dom F B =
3 1 2 ax-mp F B = dom F B =
4 dmres dom F B = B dom F
5 incom B dom F = dom F B
6 4 5 eqtri dom F B = dom F B
7 fndm F Fn A dom F = A
8 7 ineq1d F Fn A dom F B = A B
9 6 8 syl5eq F Fn A dom F B = A B
10 9 eqeq1d F Fn A dom F B = A B =
11 3 10 syl5rbb F Fn A A B = F B =