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	⊢ ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		csbeq1	⊢ ( 𝑧 = 𝐴 → ⦋ 𝑧 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) )
2		dfsbcq2	⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
3	2	iotabidv	⊢ ( 𝑧 = 𝐴 → ( ℩ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 ) = ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 ) )
4	1 3	eqeq12d	⊢ ( 𝑧 = 𝐴 → ( ⦋ 𝑧 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ( ℩ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 ) ) )
5		vex	⊢ 𝑧 ∈ V
6		nfs1v	⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑
7	6	nfiotaw	⊢ Ⅎ 𝑥 ( ℩ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 )
8		sbequ12	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
9	8	iotabidv	⊢ ( 𝑥 = 𝑧 → ( ℩ 𝑦 𝜑 ) = ( ℩ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 ) )
10	5 7 9	csbief	⊢ ⦋ 𝑧 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ( ℩ 𝑦 [ 𝑧 / 𝑥 ] 𝜑 )
11	4 10	vtoclg	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 ) )
12		csbprc	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ∅ )
13		sbcex	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V )
14	13	con3i	⊢ ( ¬ 𝐴 ∈ V → ¬ [ 𝐴 / 𝑥 ] 𝜑 )
15	14	nexdv	⊢ ( ¬ 𝐴 ∈ V → ¬ ∃ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )
16		euex	⊢ ( ∃! 𝑦 [ 𝐴 / 𝑥 ] 𝜑 → ∃ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )
17	16	con3i	⊢ ( ¬ ∃ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 → ¬ ∃! 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )
18		iotanul	⊢ ( ¬ ∃! 𝑦 [ 𝐴 / 𝑥 ] 𝜑 → ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 ) = ∅ )
19	15 17 18	3syl	⊢ ( ¬ 𝐴 ∈ V → ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 ) = ∅ )
20	12 19	eqtr4d	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 ) )
21	11 20	pm2.61i	⊢ ⦋ 𝐴 / 𝑥 ⦌ ( ℩ 𝑦 𝜑 ) = ( ℩ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )