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 
|- ( A e. _V -> [_ A / x ]_ << C , D >> = << [_ A / x ]_ C , [_ A / x ]_ D >> )

Proof

Step Hyp Ref Expression
1 nfcsb1v 
 |-  F/_ x [_ A / x ]_ C
2 nfcsb1v 
 |-  F/_ x [_ A / x ]_ D
3 1 2 nfaltop 
 |-  F/_ x << [_ A / x ]_ C , [_ A / x ]_ D >>
4 3 a1i 
 |-  ( A e. _V -> F/_ x << [_ A / x ]_ C , [_ A / x ]_ D >> )
5 csbeq1a 
 |-  ( x = A -> C = [_ A / x ]_ C )
6 altopeq1 
 |-  ( C = [_ A / x ]_ C -> << C , D >> = << [_ A / x ]_ C , D >> )
7 5 6 syl 
 |-  ( x = A -> << C , D >> = << [_ A / x ]_ C , D >> )
8 csbeq1a 
 |-  ( x = A -> D = [_ A / x ]_ D )
9 altopeq2 
 |-  ( D = [_ A / x ]_ D -> << [_ A / x ]_ C , D >> = << [_ A / x ]_ C , [_ A / x ]_ D >> )
10 8 9 syl 
 |-  ( x = A -> << [_ A / x ]_ C , D >> = << [_ A / x ]_ C , [_ A / x ]_ D >> )
11 7 10 eqtrd 
 |-  ( x = A -> << C , D >> = << [_ A / x ]_ C , [_ A / x ]_ D >> )
12 4 11 csbiegf 
 |-  ( A e. _V -> [_ A / x ]_ << C , D >> = << [_ A / x ]_ C , [_ A / x ]_ D >> )