Theorem relresOLD

Description: Obsolete version of relres as of 16-Oct-2026. (Contributed by NM, 2-Aug-1994) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	relresOLD	$$⊢\mathrm{Rel}\left({A\upharpoonright }_B\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-res	$$⊢{A\upharpoonright }_B=A\cap \left(B\times \mathrm{V}\right)$$
2		inss2	$$⊢A\cap \left(B\times \mathrm{V}\right)\subseteq B\times \mathrm{V}$$
3	1 2	eqsstri	$$⊢{A\upharpoonright }_B\subseteq B\times \mathrm{V}$$
4		relxp	$$⊢\mathrm{Rel}\left(B\times \mathrm{V}\right)$$
5		relss	$$⊢{A\upharpoonright }_B\subseteq B\times \mathrm{V}\to \left(\mathrm{Rel}\left(B\times \mathrm{V}\right)\to \mathrm{Rel}\left({A\upharpoonright }_B\right)\right)$$
6	3 4 5	mp2	$$⊢\mathrm{Rel}\left({A\upharpoonright }_B\right)$$