csbfv

Description: Substitution for a function value. (Contributed by NM, 1-Jan-2006) (Revised by NM, 20-Aug-2018)

		Ref	Expression
	Assertion	csbfv	$⊢ ⦋ A / x ⦌ F (x) = F (A)$

Step	Hyp	Ref	Expression
1		csbfv2g	$⊢ A \in V \to ⦋ A / x ⦌ F (x) = F (⦋ A / x ⦌ x)$
2		csbvarg	$⊢ A \in V \to ⦋ A / x ⦌ x = A$
3	2	fveq2d	$⊢ A \in V \to F (⦋ A / x ⦌ x) = F (A)$
4	1 3	eqtrd	$⊢ A \in V \to ⦋ A / x ⦌ F (x) = F (A)$
5		csbprc	$⊢ \neg A \in V \to ⦋ A / x ⦌ F (x) = \emptyset$
6		fvprc	$⊢ \neg A \in V \to F (A) = \emptyset$
7	5 6	eqtr4d	$⊢ \neg A \in V \to ⦋ A / x ⦌ F (x) = F (A)$
8	4 7	pm2.61i	$⊢ ⦋ A / x ⦌ F (x) = F (A)$

Metamath Proof Explorer