Theorem dfres4

Description: Alternate definition of the restriction of a class. (Contributed by Peter Mazsa, 2-Jan-2019)

	Ref	Expression
Assertion	dfres4	$$⊢{R\upharpoonright }_A=R\cap \left(A\times \mathrm{ran}\left({R\upharpoonright }_A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfres2	$$⊢{R\upharpoonright }_A=\left\{⟨x,y⟩|\left(x\in A\wedge xRy\right)\right\}$$
2		inxprnres	$$⊢R\cap \left(A\times \mathrm{ran}\left({R\upharpoonright }_A\right)\right)=\left\{⟨x,y⟩|\left(x\in A\wedge xRy\right)\right\}$$
3	1 2	eqtr4i	$$⊢{R\upharpoonright }_A=R\cap \left(A\times \mathrm{ran}\left({R\upharpoonright }_A\right)\right)$$