Metamath Proof Explorer


Theorem resindm

Description: When restricting a class, intersecting with the domain of the class has no effect. (Contributed by FL, 6-Oct-2008) Remove antecedent. (Revised by Eric Schmidt, 16-Jun-2026)

Ref Expression
Assertion resindm A B dom A = A B

Proof

Step Hyp Ref Expression
1 dmres dom A B = B dom A
2 1 reseq2i A B dom A B = A B B dom A
3 relres Rel A B
4 resdm Rel A B A B dom A B = A B
5 3 4 ax-mp A B dom A B = A B
6 inss1 B dom A B
7 6 resabs1i A B B dom A = A B dom A
8 2 5 7 3eqtr3ri A B dom A = A B