Theorem csbif

Description: Distribute proper substitution through the conditional operator. (Contributed by NM, 24-Feb-2013) (Revised by NM, 19-Aug-2018)

	Ref	Expression
Assertion	csbif	$$⊢⦋A/x⦌if\left(\phi ,B,C\right)=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,⦋A/x⦌B,⦋A/x⦌C\right)$$

Proof

Step	Hyp	Ref	Expression
1		csbeq1	$$⊢y=A\to ⦋y/x⦌if\left(\phi ,B,C\right)=⦋A/x⦌if\left(\phi ,B,C\right)$$
2		dfsbcq2	$$⊢y=A\to \left(\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
3		csbeq1	$$⊢y=A\to ⦋y/x⦌B=⦋A/x⦌B$$
4		csbeq1	$$⊢y=A\to ⦋y/x⦌C=⦋A/x⦌C$$
5	2 3 4	ifbieq12d	$$⊢y=A\to if\left(\left[y/x\right]\phi ,⦋y/x⦌B,⦋y/x⦌C\right)=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,⦋A/x⦌B,⦋A/x⦌C\right)$$
6	1 5	eqeq12d	$$⊢y=A\to \left(⦋y/x⦌if\left(\phi ,B,C\right)=if\left(\left[y/x\right]\phi ,⦋y/x⦌B,⦋y/x⦌C\right)\leftrightarrow ⦋A/x⦌if\left(\phi ,B,C\right)=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,⦋A/x⦌B,⦋A/x⦌C\right)\right)$$
7		vex	$$⊢y\in \mathrm{V}$$
8		nfs1v	$$⊢Ⅎx\left[y/x\right]\phi$$
9		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
10		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌C$$
11	8 9 10	nfif	$$⊢\underset{\_}{Ⅎ}xif\left(\left[y/x\right]\phi ,⦋y/x⦌B,⦋y/x⦌C\right)$$
12		sbequ12	$$⊢x=y\to \left(\phi \leftrightarrow \left[y/x\right]\phi \right)$$
13		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
14		csbeq1a	$$⊢x=y\to C=⦋y/x⦌C$$
15	12 13 14	ifbieq12d	$$⊢x=y\to if\left(\phi ,B,C\right)=if\left(\left[y/x\right]\phi ,⦋y/x⦌B,⦋y/x⦌C\right)$$
16	7 11 15	csbief	$$⊢⦋y/x⦌if\left(\phi ,B,C\right)=if\left(\left[y/x\right]\phi ,⦋y/x⦌B,⦋y/x⦌C\right)$$
17	6 16	vtoclg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌if\left(\phi ,B,C\right)=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,⦋A/x⦌B,⦋A/x⦌C\right)$$
18		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌if\left(\phi ,B,C\right)=\varnothing$$
19		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B=\varnothing$$
20		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌C=\varnothing$$
21	19 20	ifeq12d	$$⊢\neg A\in \mathrm{V}\to if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,⦋A/x⦌B,⦋A/x⦌C\right)=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\varnothing ,\varnothing \right)$$
22		ifid	$$⊢if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,\varnothing ,\varnothing \right)=\varnothing$$
23	21 22	syl6req	$$⊢\neg A\in \mathrm{V}\to \varnothing =if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,⦋A/x⦌B,⦋A/x⦌C\right)$$
24	18 23	eqtrd	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌if\left(\phi ,B,C\right)=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,⦋A/x⦌B,⦋A/x⦌C\right)$$
25	17 24	pm2.61i	$$⊢⦋A/x⦌if\left(\phi ,B,C\right)=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi ,⦋A/x⦌B,⦋A/x⦌C\right)$$