Theorem eqres

Description: Converting a class constant definition by restriction (like df-ers or df-parts ) into a binary relation. (Contributed by Peter Mazsa, 1-Oct-2018)

	Ref	Expression
Hypothesis	eqres.1	$$⊢R={S\upharpoonright }_C$$
Assertion	eqres	$$⊢B\in V\to \left(ARB\leftrightarrow \left(A\in C\wedge ASB\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqres.1	$$⊢R={S\upharpoonright }_C$$
2	1	breqi	$$⊢ARB\leftrightarrow A\left({S\upharpoonright }_C\right)B$$
3		brres	$$⊢B\in V\to \left(A\left({S\upharpoonright }_C\right)B\leftrightarrow \left(A\in C\wedge ASB\right)\right)$$
4	2 3	bitrid	$$⊢B\in V\to \left(ARB\leftrightarrow \left(A\in C\wedge ASB\right)\right)$$