Theorem brinxprnres

Description: Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019)

	Ref	Expression
Assertion	brinxprnres	$$⊢C\in V\to \left(B\left(R\cap \left(A\times \mathrm{ran}\left({R\upharpoonright }_A\right)\right)\right)C\leftrightarrow \left(B\in A\wedge BRC\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		brres2	$$⊢B\left({R\upharpoonright }_A\right)C\leftrightarrow B\left(R\cap \left(A\times \mathrm{ran}\left({R\upharpoonright }_A\right)\right)\right)C$$
2		brres	$$⊢C\in V\to \left(B\left({R\upharpoonright }_A\right)C\leftrightarrow \left(B\in A\wedge BRC\right)\right)$$
3	1 2	bitr3id	$$⊢C\in V\to \left(B\left(R\cap \left(A\times \mathrm{ran}\left({R\upharpoonright }_A\right)\right)\right)C\leftrightarrow \left(B\in A\wedge BRC\right)\right)$$