Theorem sbcaltop

Description: Distribution of class substitution over alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015)

	Ref	Expression
Assertion	sbcaltop	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ⟪ 𝐶 , 𝐷 ⟫ = ⟪ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ⟫ )

Proof

Step	Hyp	Ref	Expression
1		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝐴 / 𝑥 ⦌ 𝐶
2		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝐴 / 𝑥 ⦌ 𝐷
3	1 2	nfaltop	⊢ Ⅎ 𝑥 ⟪ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ⟫
4	3	a1i	⊢ ( 𝐴 ∈ V → Ⅎ 𝑥 ⟪ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ⟫ )
5		csbeq1a	⊢ ( 𝑥 = 𝐴 → 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
6		altopeq1	⊢ ( 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 → ⟪ 𝐶 , 𝐷 ⟫ = ⟪ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , 𝐷 ⟫ )
7	5 6	syl	⊢ ( 𝑥 = 𝐴 → ⟪ 𝐶 , 𝐷 ⟫ = ⟪ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , 𝐷 ⟫ )
8		csbeq1a	⊢ ( 𝑥 = 𝐴 → 𝐷 = ⦋ 𝐴 / 𝑥 ⦌ 𝐷 )
9		altopeq2	⊢ ( 𝐷 = ⦋ 𝐴 / 𝑥 ⦌ 𝐷 → ⟪ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , 𝐷 ⟫ = ⟪ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ⟫ )
10	8 9	syl	⊢ ( 𝑥 = 𝐴 → ⟪ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , 𝐷 ⟫ = ⟪ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ⟫ )
11	7 10	eqtrd	⊢ ( 𝑥 = 𝐴 → ⟪ 𝐶 , 𝐷 ⟫ = ⟪ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ⟫ )
12	4 11	csbiegf	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ ⟪ 𝐶 , 𝐷 ⟫ = ⟪ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ⟫ )