csbov

Description: Move class substitution in and out of an operation. (Contributed by NM, 23-Aug-2018)

		Ref	Expression
	Assertion	csbov	$⊢ ⦋ A / x ⦌ (B F C) = B ⦋ A / x ⦌ F C$

Step	Hyp	Ref	Expression
1		csbov123	$⊢ ⦋ A / x ⦌ (B F C) = ⦋ A / x ⦌ B ⦋ A / x ⦌ F ⦋ A / x ⦌ C$
2		csbconstg	$⊢ A \in V \to ⦋ A / x ⦌ B = B$
3		csbconstg	$⊢ A \in V \to ⦋ A / x ⦌ C = C$
4	2 3	oveq12d	$⊢ A \in V \to ⦋ A / x ⦌ B ⦋ A / x ⦌ F ⦋ A / x ⦌ C = B ⦋ A / x ⦌ F C$
5		0fv	$⊢ \emptyset (⟨B, C⟩) = \emptyset$
6		df-ov	$⊢ B \emptyset C = \emptyset (⟨B, C⟩)$
7		0ov	$⊢ ⦋ A / x ⦌ B \emptyset ⦋ A / x ⦌ C = \emptyset$
8	5 6 7	3eqtr4ri	$⊢ ⦋ A / x ⦌ B \emptyset ⦋ A / x ⦌ C = B \emptyset C$
9		csbprc	$⊢ \neg A \in V \to ⦋ A / x ⦌ F = \emptyset$
10	9	oveqd	$⊢ \neg A \in V \to ⦋ A / x ⦌ B ⦋ A / x ⦌ F ⦋ A / x ⦌ C = ⦋ A / x ⦌ B \emptyset ⦋ A / x ⦌ C$
11	9	oveqd	$⊢ \neg A \in V \to B ⦋ A / x ⦌ F C = B \emptyset C$
12	8 10 11	3eqtr4a	$⊢ \neg A \in V \to ⦋ A / x ⦌ B ⦋ A / x ⦌ F ⦋ A / x ⦌ C = B ⦋ A / x ⦌ F C$
13	4 12	pm2.61i	$⊢ ⦋ A / x ⦌ B ⦋ A / x ⦌ F ⦋ A / x ⦌ C = B ⦋ A / x ⦌ F C$
14	1 13	eqtri	$⊢ ⦋ A / x ⦌ (B F C) = B ⦋ A / x ⦌ F C$

Metamath Proof Explorer