Theorem csbiota

Description: Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017) (Revised by NM, 23-Aug-2018)

	Ref	Expression
Assertion	csbiota	$$⊢⦋A/x⦌\left(\iota y|\phi \right)=\left(\iota y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		csbeq1	$$⊢z=A\to ⦋z/x⦌\left(\iota y|\phi \right)=⦋A/x⦌\left(\iota y|\phi \right)$$
2		dfsbcq2	$$⊢z=A\to \left(\left[z/x\right]\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
3	2	iotabidv	$$⊢z=A\to \left(\iota y|\left[z/x\right]\phi \right)=\left(\iota y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
4	1 3	eqeq12d	$$⊢z=A\to \left(⦋z/x⦌\left(\iota y|\phi \right)=\left(\iota y|\left[z/x\right]\phi \right)\leftrightarrow ⦋A/x⦌\left(\iota y|\phi \right)=\left(\iota y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
5		vex	$$⊢z\in \mathrm{V}$$
6		nfs1v	$$⊢Ⅎx\left[z/x\right]\phi$$
7	6	nfiotaw	$$⊢\underset{\_}{Ⅎ}x\left(\iota y|\left[z/x\right]\phi \right)$$
8		sbequ12	$$⊢x=z\to \left(\phi \leftrightarrow \left[z/x\right]\phi \right)$$
9	8	iotabidv	$$⊢x=z\to \left(\iota y|\phi \right)=\left(\iota y|\left[z/x\right]\phi \right)$$
10	5 7 9	csbief	$$⊢⦋z/x⦌\left(\iota y|\phi \right)=\left(\iota y|\left[z/x\right]\phi \right)$$
11	4 10	vtoclg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌\left(\iota y|\phi \right)=\left(\iota y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
12		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌\left(\iota y|\phi \right)=\varnothing$$
13		sbcex	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to A\in \mathrm{V}$$
14	13	con3i	$$⊢\neg A\in \mathrm{V}\to \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
15	14	nexdv	$$⊢\neg A\in \mathrm{V}\to \neg \exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
16		euex	$$⊢\exists !y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
17	16	con3i	$$⊢\neg \exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \neg \exists !y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
18		iotanul	$$⊢\neg \exists !y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \left(\iota y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)=\varnothing$$
19	15 17 18	3syl	$$⊢\neg A\in \mathrm{V}\to \left(\iota y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)=\varnothing$$
20	12 19	eqtr4d	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌\left(\iota y|\phi \right)=\left(\iota y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
21	11 20	pm2.61i	$$⊢⦋A/x⦌\left(\iota y|\phi \right)=\left(\iota y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$