Theorem csbnestgfw

Description: Nest the composition of two substitutions. Version of csbnestgf with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 23-Nov-2005) (Revised by Gino Giotto, 26-Jan-2024)

	Ref	Expression
Assertion	csbnestgfw	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 Ⅎ 𝑥 𝐶 ) → ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = ⦋ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ⦌ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2		df-csb	⊢ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = { 𝑧 ∣ [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 }
3	2	abeq2i	⊢ ( 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 ↔ [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 )
4	3	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 )
5		nfcr	⊢ ( Ⅎ 𝑥 𝐶 → Ⅎ 𝑥 𝑧 ∈ 𝐶 )
6	5	alimi	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝐶 → ∀ 𝑦 Ⅎ 𝑥 𝑧 ∈ 𝐶 )
7		sbcnestgfw	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑦 Ⅎ 𝑥 𝑧 ∈ 𝐶 ) → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 ) )
8	6 7	sylan2	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑦 Ⅎ 𝑥 𝐶 ) → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 ) )
9	4 8	syl5bb	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑦 Ⅎ 𝑥 𝐶 ) → ( [ 𝐴 / 𝑥 ] 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 ) )
10	9	abbidv	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑦 Ⅎ 𝑥 𝐶 ) → { 𝑧 ∣ [ 𝐴 / 𝑥 ] 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 } = { 𝑧 ∣ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 } )
11	1 10	sylan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 Ⅎ 𝑥 𝐶 ) → { 𝑧 ∣ [ 𝐴 / 𝑥 ] 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 } = { 𝑧 ∣ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 } )
12		df-csb	⊢ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = { 𝑧 ∣ [ 𝐴 / 𝑥 ] 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 }
13		df-csb	⊢ ⦋ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ⦌ 𝐶 = { 𝑧 ∣ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 }
14	11 12 13	3eqtr4g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 Ⅎ 𝑥 𝐶 ) → ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = ⦋ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ⦌ 𝐶 )