Theorem csbdm

Description: Distribute proper substitution through the domain of a class. (Contributed by Alexander van der Vekens, 23-Jul-2017) (Revised by NM, 24-Aug-2018)

	Ref	Expression
Assertion	csbdm	⊢ ⦋ 𝐴 / 𝑥 ⦌ dom 𝐵 = dom ⦋ 𝐴 / 𝑥 ⦌ 𝐵

Proof

Step	Hyp	Ref	Expression
1		csbab	⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 }
2		sbcex2	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 [ 𝐴 / 𝑥 ] ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 )
3		sbcel2	⊢ ( [ 𝐴 / 𝑥 ] ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 ↔ ⟨ 𝑦 , 𝑤 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
4	3	exbii	⊢ ( ∃ 𝑤 [ 𝐴 / 𝑥 ] ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
5	2 4	bitri	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 ↔ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
6	5	abbii	⊢ { 𝑦 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 }
7	1 6	eqtri	⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 } = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 }
8		dfdm3	⊢ dom 𝐵 = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 }
9	8	csbeq2i	⊢ ⦋ 𝐴 / 𝑥 ⦌ dom 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ 𝐵 }
10		dfdm3	⊢ dom ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑦 ∣ ∃ 𝑤 ⟨ 𝑦 , 𝑤 ⟩ ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 }
11	7 9 10	3eqtr4i	⊢ ⦋ 𝐴 / 𝑥 ⦌ dom 𝐵 = dom ⦋ 𝐴 / 𝑥 ⦌ 𝐵