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 >. ) |