Metamath Proof Explorer

Theorem ssdmres

Description: A domain restricted to a subclass equals the subclass. (Contributed by NM, 2-Mar-1997)

Ref Expression
Assertion ssdmres A dom B dom B A = A


Step Hyp Ref Expression
1 df-ss A dom B A dom B = A
2 dmres dom B A = A dom B
3 2 eqeq1i dom B A = A A dom B = A
4 1 3 bitr4i A dom B dom B A = A