Theorem sbcrel

Description: Distribute proper substitution through a relation predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017)

	Ref	Expression
Assertion	sbcrel	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Rel}R\leftrightarrow \mathrm{Rel}⦋A/x⦌R\right)$$

Proof

Step	Hyp	Ref	Expression
1		sbcssg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}R\subseteq \mathrm{V}\times \mathrm{V}\leftrightarrow ⦋A/x⦌R\subseteq ⦋A/x⦌\left(\mathrm{V}\times \mathrm{V}\right)\right)$$
2		csbconstg	$$⊢A\in V\to ⦋A/x⦌\left(\mathrm{V}\times \mathrm{V}\right)=\mathrm{V}\times \mathrm{V}$$
3	2	sseq2d	$$⊢A\in V\to \left(⦋A/x⦌R\subseteq ⦋A/x⦌\left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow ⦋A/x⦌R\subseteq \mathrm{V}\times \mathrm{V}\right)$$
4	1 3	bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}R\subseteq \mathrm{V}\times \mathrm{V}\leftrightarrow ⦋A/x⦌R\subseteq \mathrm{V}\times \mathrm{V}\right)$$
5		df-rel	$$⊢\mathrm{Rel}R\leftrightarrow R\subseteq \mathrm{V}\times \mathrm{V}$$
6	5	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Rel}R\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}R\subseteq \mathrm{V}\times \mathrm{V}$$
7		df-rel	$$⊢\mathrm{Rel}⦋A/x⦌R\leftrightarrow ⦋A/x⦌R\subseteq \mathrm{V}\times \mathrm{V}$$
8	4 6 7	3bitr4g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\mathrm{Rel}R\leftrightarrow \mathrm{Rel}⦋A/x⦌R\right)$$