Theorem sbcnestgfw

Description: Nest the composition of two substitutions. Version of sbcnestgf with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 11-Nov-2016) (Revised by Gino Giotto, 26-Jan-2024)

	Ref	Expression
Assertion	sbcnestgfw	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 Ⅎ 𝑥 𝜑 ) → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		dfsbcq	⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ) )
2		csbeq1	⊢ ( 𝑧 = 𝐴 → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
3	2	sbceq1d	⊢ ( 𝑧 = 𝐴 → ( [ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝜑 ) )
4	1 3	bibi12d	⊢ ( 𝑧 = 𝐴 → ( ( [ 𝑧 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝜑 ) ↔ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝜑 ) ) )
5	4	imbi2d	⊢ ( 𝑧 = 𝐴 → ( ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( [ 𝑧 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝜑 ) ) ↔ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝜑 ) ) ) )
6		vex	⊢ 𝑧 ∈ V
7	6	a1i	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → 𝑧 ∈ V )
8		csbeq1a	⊢ ( 𝑥 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
9	8	sbceq1d	⊢ ( 𝑥 = 𝑧 → ( [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝜑 ) )
10	9	adantl	⊢ ( ( ∀ 𝑦 Ⅎ 𝑥 𝜑 ∧ 𝑥 = 𝑧 ) → ( [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝜑 ) )
11		nfnf1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝜑
12	11	nfal	⊢ Ⅎ 𝑥 ∀ 𝑦 Ⅎ 𝑥 𝜑
13		nfa1	⊢ Ⅎ 𝑦 ∀ 𝑦 Ⅎ 𝑥 𝜑
14		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
15	14	a1i	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
16		sp	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → Ⅎ 𝑥 𝜑 )
17	13 15 16	nfsbcdw	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → Ⅎ 𝑥 [ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝜑 )
18	7 10 12 17	sbciedf	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( [ 𝑧 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝜑 ) )
19	5 18	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 Ⅎ 𝑥 𝜑 → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝜑 ) ) )
20	19	imp	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 Ⅎ 𝑥 𝜑 ) → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] 𝜑 ) )