Metamath Proof Explorer


Theorem sbcaltop

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

Ref Expression
Assertion sbcaltop AVA/xCD=A/xCA/xD

Proof

Step Hyp Ref Expression
1 nfcsb1v _xA/xC
2 nfcsb1v _xA/xD
3 1 2 nfaltop _xA/xCA/xD
4 3 a1i AV_xA/xCA/xD
5 csbeq1a x=AC=A/xC
6 altopeq1 C=A/xCCD=A/xCD
7 5 6 syl x=ACD=A/xCD
8 csbeq1a x=AD=A/xD
9 altopeq2 D=A/xDA/xCD=A/xCA/xD
10 8 9 syl x=AA/xCD=A/xCA/xD
11 7 10 eqtrd x=ACD=A/xCA/xD
12 4 11 csbiegf AVA/xCD=A/xCA/xD