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