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 ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ⟩ )

Proof

Step Hyp Ref Expression
1 csbif ⊢ ⦋ 𝐴 / 𝑥 ⦌ if ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) , { { 𝐶 } , { 𝐶 , 𝐷 } } , ∅ ) = if ( [ 𝐴 / 𝑥 ] ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) , ⦋ 𝐴 / 𝑥 ⦌ { { 𝐶 } , { 𝐶 , 𝐷 } } , ⦋ 𝐴 / 𝑥 ⦌ ∅ )
2 sbcan ⊢ ( [ 𝐴 / 𝑥 ] ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ↔ ( [ 𝐴 / 𝑥 ] 𝐶 ∈ V ∧ [ 𝐴 / 𝑥 ] 𝐷 ∈ V ) )
3 sbcel1g ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐶 ∈ V ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ V ) )
4 sbcel1g ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐷 ∈ V ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∈ V ) )
5 3 4 anbi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝐶 ∈ V ∧ [ 𝐴 / 𝑥 ] 𝐷 ∈ V ) ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ V ∧ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∈ V ) ) )
6 2 5 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ V ∧ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∈ V ) ) )
7 csbprg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { { 𝐶 } , { 𝐶 , 𝐷 } } = { ⦋ 𝐴 / 𝑥 ⦌ { 𝐶 } , ⦋ 𝐴 / 𝑥 ⦌ { 𝐶 , 𝐷 } } )
8 csbsng ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝐶 } = { ⦋ 𝐴 / 𝑥 ⦌ 𝐶 } )
9 csbprg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝐶 , 𝐷 } = { ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 } )
10 8 9 preq12d ⊢ ( 𝐴 ∈ 𝑉 → { ⦋ 𝐴 / 𝑥 ⦌ { 𝐶 } , ⦋ 𝐴 / 𝑥 ⦌ { 𝐶 , 𝐷 } } = { { ⦋ 𝐴 / 𝑥 ⦌ 𝐶 } , { ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 } } )
11 7 10 eqtrd ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { { 𝐶 } , { 𝐶 , 𝐷 } } = { { ⦋ 𝐴 / 𝑥 ⦌ 𝐶 } , { ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 } } )
12 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ∅ = ∅ )
13 6 11 12 ifbieq12d ⊢ ( 𝐴 ∈ 𝑉 → if ( [ 𝐴 / 𝑥 ] ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) , ⦋ 𝐴 / 𝑥 ⦌ { { 𝐶 } , { 𝐶 , 𝐷 } } , ⦋ 𝐴 / 𝑥 ⦌ ∅ ) = if ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ V ∧ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∈ V ) , { { ⦋ 𝐴 / 𝑥 ⦌ 𝐶 } , { ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 } } , ∅ ) )
14 1 13 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ if ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) , { { 𝐶 } , { 𝐶 , 𝐷 } } , ∅ ) = if ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ V ∧ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∈ V ) , { { ⦋ 𝐴 / 𝑥 ⦌ 𝐶 } , { ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 } } , ∅ ) )
15 dfopif ⊢ ⟨ 𝐶 , 𝐷 ⟩ = if ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) , { { 𝐶 } , { 𝐶 , 𝐷 } } , ∅ )
16 15 csbeq2i ⊢ ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝐶 , 𝐷 ⟩ = ⦋ 𝐴 / 𝑥 ⦌ if ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) , { { 𝐶 } , { 𝐶 , 𝐷 } } , ∅ )
17 dfopif ⊢ ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ⟩ = if ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ V ∧ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∈ V ) , { { ⦋ 𝐴 / 𝑥 ⦌ 𝐶 } , { ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 } } , ∅ )
18 14 16 17 3eqtr4g ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ⟩ )