Theorem sbcaltop

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

	Ref	Expression
Assertion	sbcaltop	$$⊢A\in \mathrm{V}\to ⦋A/x⦌⟪C,D⟫=⟪⦋A/x⦌C,⦋A/x⦌D⟫$$

Proof

Step	Hyp	Ref	Expression
1		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋A/x⦌C$$
2		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋A/x⦌D$$
3	1 2	nfaltop	$$⊢\underset{\_}{Ⅎ}x⟪⦋A/x⦌C,⦋A/x⦌D⟫$$
4	3	a1i	$$⊢A\in \mathrm{V}\to \underset{\_}{Ⅎ}x⟪⦋A/x⦌C,⦋A/x⦌D⟫$$
5		csbeq1a	$$⊢x=A\to C=⦋A/x⦌C$$
6		altopeq1	$$⊢C=⦋A/x⦌C\to ⟪C,D⟫=⟪⦋A/x⦌C,D⟫$$
7	5 6	syl	$$⊢x=A\to ⟪C,D⟫=⟪⦋A/x⦌C,D⟫$$
8		csbeq1a	$$⊢x=A\to D=⦋A/x⦌D$$
9		altopeq2	$$⊢D=⦋A/x⦌D\to ⟪⦋A/x⦌C,D⟫=⟪⦋A/x⦌C,⦋A/x⦌D⟫$$
10	8 9	syl	$$⊢x=A\to ⟪⦋A/x⦌C,D⟫=⟪⦋A/x⦌C,⦋A/x⦌D⟫$$
11	7 10	eqtrd	$$⊢x=A\to ⟪C,D⟫=⟪⦋A/x⦌C,⦋A/x⦌D⟫$$
12	4 11	csbiegf	$$⊢A\in \mathrm{V}\to ⦋A/x⦌⟪C,D⟫=⟪⦋A/x⦌C,⦋A/x⦌D⟫$$