Theorem csbnestgf

Description: Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker csbnestgfw when possible. (Contributed by NM, 23-Nov-2005) (Proof shortened by Mario Carneiro, 10-Nov-2016) (New usage is discouraged.)

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

Proof

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