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 (\underset{˙}{[} A / x \underset{˙}{]} Rel R \leftrightarrow Rel ⦋ A / x ⦌ R)$

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

Metamath Proof Explorer