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