This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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