Metamath Proof Explorer


Theorem csbopg

Description: Distribution of class substitution over ordered pairs. (Contributed by Drahflow, 25-Sep-2015) (Revised by Mario Carneiro, 29-Oct-2015) (Revised by ML, 25-Oct-2020)

Ref Expression
Assertion csbopg
|- ( A e. V -> [_ A / x ]_ <. C , D >. = <. [_ A / x ]_ C , [_ A / x ]_ D >. )

Proof

Step Hyp Ref Expression
1 csbif
 |-  [_ A / x ]_ if ( ( C e. _V /\ D e. _V ) , { { C } , { C , D } } , (/) ) = if ( [. A / x ]. ( C e. _V /\ D e. _V ) , [_ A / x ]_ { { C } , { C , D } } , [_ A / x ]_ (/) )
2 sbcan
 |-  ( [. A / x ]. ( C e. _V /\ D e. _V ) <-> ( [. A / x ]. C e. _V /\ [. A / x ]. D e. _V ) )
3 sbcel1g
 |-  ( A e. V -> ( [. A / x ]. C e. _V <-> [_ A / x ]_ C e. _V ) )
4 sbcel1g
 |-  ( A e. V -> ( [. A / x ]. D e. _V <-> [_ A / x ]_ D e. _V ) )
5 3 4 anbi12d
 |-  ( A e. V -> ( ( [. A / x ]. C e. _V /\ [. A / x ]. D e. _V ) <-> ( [_ A / x ]_ C e. _V /\ [_ A / x ]_ D e. _V ) ) )
6 2 5 syl5bb
 |-  ( A e. V -> ( [. A / x ]. ( C e. _V /\ D e. _V ) <-> ( [_ A / x ]_ C e. _V /\ [_ A / x ]_ D e. _V ) ) )
7 csbprg
 |-  ( A e. V -> [_ A / x ]_ { { C } , { C , D } } = { [_ A / x ]_ { C } , [_ A / x ]_ { C , D } } )
8 csbsng
 |-  ( A e. V -> [_ A / x ]_ { C } = { [_ A / x ]_ C } )
9 csbprg
 |-  ( A e. V -> [_ A / x ]_ { C , D } = { [_ A / x ]_ C , [_ A / x ]_ D } )
10 8 9 preq12d
 |-  ( A e. V -> { [_ A / x ]_ { C } , [_ A / x ]_ { C , D } } = { { [_ A / x ]_ C } , { [_ A / x ]_ C , [_ A / x ]_ D } } )
11 7 10 eqtrd
 |-  ( A e. V -> [_ A / x ]_ { { C } , { C , D } } = { { [_ A / x ]_ C } , { [_ A / x ]_ C , [_ A / x ]_ D } } )
12 csbconstg
 |-  ( A e. V -> [_ A / x ]_ (/) = (/) )
13 6 11 12 ifbieq12d
 |-  ( A e. V -> if ( [. A / x ]. ( C e. _V /\ D e. _V ) , [_ A / x ]_ { { C } , { C , D } } , [_ A / x ]_ (/) ) = if ( ( [_ A / x ]_ C e. _V /\ [_ A / x ]_ D e. _V ) , { { [_ A / x ]_ C } , { [_ A / x ]_ C , [_ A / x ]_ D } } , (/) ) )
14 1 13 eqtrid
 |-  ( A e. V -> [_ A / x ]_ if ( ( C e. _V /\ D e. _V ) , { { C } , { C , D } } , (/) ) = if ( ( [_ A / x ]_ C e. _V /\ [_ A / x ]_ D e. _V ) , { { [_ A / x ]_ C } , { [_ A / x ]_ C , [_ A / x ]_ D } } , (/) ) )
15 dfopif
 |-  <. C , D >. = if ( ( C e. _V /\ D e. _V ) , { { C } , { C , D } } , (/) )
16 15 csbeq2i
 |-  [_ A / x ]_ <. C , D >. = [_ A / x ]_ if ( ( C e. _V /\ D e. _V ) , { { C } , { C , D } } , (/) )
17 dfopif
 |-  <. [_ A / x ]_ C , [_ A / x ]_ D >. = if ( ( [_ A / x ]_ C e. _V /\ [_ A / x ]_ D e. _V ) , { { [_ A / x ]_ C } , { [_ A / x ]_ C , [_ A / x ]_ D } } , (/) )
18 14 16 17 3eqtr4g
 |-  ( A e. V -> [_ A / x ]_ <. C , D >. = <. [_ A / x ]_ C , [_ A / x ]_ D >. )