Metamath Proof Explorer


Theorem resdmdfsnOLD

Description: Obsolete version of resdmdfsn as of 16-Jun-2026. (Contributed by AV, 2-Dec-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion resdmdfsnOLD Rel R R V X = R dom R X

Proof

Step Hyp Ref Expression
1 resindmOLD Rel R R V X dom R = R V X
2 indif1 V X dom R = V dom R X
3 incom V dom R = dom R V
4 inv1 dom R V = dom R
5 3 4 eqtri V dom R = dom R
6 5 difeq1i V dom R X = dom R X
7 2 6 eqtri V X dom R = dom R X
8 7 reseq2i R V X dom R = R dom R X
9 1 8 eqtr3di Rel R R V X = R dom R X