Theorem csbriota

Description: Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013) (Revised by NM, 2-Sep-2018)

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

Proof

Step	Hyp	Ref	Expression
1		csbeq1	$$⊢z=A\to ⦋z/x⦌\left(\iota y\in B|\phi \right)=⦋A/x⦌\left(\iota y\in B|\phi \right)$$
2		dfsbcq2	$$⊢z=A\to \left(\left[z/x\right]\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
3	2	riotabidv	$$⊢z=A\to \left(\iota y\in B|\left[z/x\right]\phi \right)=\left(\iota y\in B|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
4	1 3	eqeq12d	$$⊢z=A\to \left(⦋z/x⦌\left(\iota y\in B|\phi \right)=\left(\iota y\in B|\left[z/x\right]\phi \right)\leftrightarrow ⦋A/x⦌\left(\iota y\in B|\phi \right)=\left(\iota y\in B|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
5		vex	$$⊢z\in \mathrm{V}$$
6		nfs1v	$$⊢Ⅎx\left[z/x\right]\phi$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
8	6 7	nfriota	$$⊢\underset{\_}{Ⅎ}x\left(\iota y\in B|\left[z/x\right]\phi \right)$$
9		sbequ12	$$⊢x=z\to \left(\phi \leftrightarrow \left[z/x\right]\phi \right)$$
10	9	riotabidv	$$⊢x=z\to \left(\iota y\in B|\phi \right)=\left(\iota y\in B|\left[z/x\right]\phi \right)$$
11	5 8 10	csbief	$$⊢⦋z/x⦌\left(\iota y\in B|\phi \right)=\left(\iota y\in B|\left[z/x\right]\phi \right)$$
12	4 11	vtoclg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌\left(\iota y\in B|\phi \right)=\left(\iota y\in B|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
13		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌\left(\iota y\in B|\phi \right)=\varnothing$$
14		df-riota	$$⊢\left(\iota y\in B|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)=\left(\iota y|\left(y\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
15		euex	$$⊢\exists !y\left(y\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\to \exists y\left(y\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
16		sbcex	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to A\in \mathrm{V}$$
17	16	adantl	$$⊢\left(y\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\to A\in \mathrm{V}$$
18	17	exlimiv	$$⊢\exists y\left(y\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\to A\in \mathrm{V}$$
19	15 18	syl	$$⊢\exists !y\left(y\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\to A\in \mathrm{V}$$
20		iotanul	$$⊢\neg \exists !y\left(y\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\to \left(\iota y|\left(y\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)=\varnothing$$
21	19 20	nsyl5	$$⊢\neg A\in \mathrm{V}\to \left(\iota y|\left(y\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)=\varnothing$$
22	14 21	syl5req	$$⊢\neg A\in \mathrm{V}\to \varnothing =\left(\iota y\in B|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
23	13 22	eqtrd	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌\left(\iota y\in B|\phi \right)=\left(\iota y\in B|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
24	12 23	pm2.61i	$$⊢⦋A/x⦌\left(\iota y\in B|\phi \right)=\left(\iota y\in B|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$