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 ∈ V → ⦋ A / x⦌ C D = ⦋ A / x⦌ C ⦋ A / x⦌ D

Proof

Step Hyp Ref Expression
1 csbif ⊢ ⦋ A / x⦌ if C ∈ V ∧ D ∈ V C C D ∅ = if [˙A / x]˙ C ∈ V ∧ D ∈ V ⦋ A / x⦌ C C D ⦋ A / x⦌ ∅
2 sbcan ⊢ [˙A / x]˙ C ∈ V ∧ D ∈ V ↔ [˙A / x]˙ C ∈ V ∧ [˙A / x]˙ D ∈ V
3 sbcel1g ⊢ A ∈ V → [˙A / x]˙ C ∈ V ↔ ⦋ A / x⦌ C ∈ V
4 sbcel1g ⊢ A ∈ V → [˙A / x]˙ D ∈ V ↔ ⦋ A / x⦌ D ∈ V
5 3 4 anbi12d ⊢ A ∈ V → [˙A / x]˙ C ∈ V ∧ [˙A / x]˙ D ∈ V ↔ ⦋ A / x⦌ C ∈ V ∧ ⦋ A / x⦌ D ∈ V
6 2 5 bitrid ⊢ A ∈ V → [˙A / x]˙ C ∈ V ∧ D ∈ V ↔ ⦋ A / x⦌ C ∈ V ∧ ⦋ A / x⦌ D ∈ V
7 csbprg ⊢ A ∈ V → ⦋ A / x⦌ C C D = ⦋ A / x⦌ C ⦋ A / x⦌ C D
8 csbsng ⊢ A ∈ V → ⦋ A / x⦌ C = ⦋ A / x⦌ C
9 csbprg ⊢ A ∈ V → ⦋ A / x⦌ C D = ⦋ A / x⦌ C ⦋ A / x⦌ D
10 8 9 preq12d ⊢ A ∈ V → ⦋ A / x⦌ C ⦋ A / x⦌ C D = ⦋ A / x⦌ C ⦋ A / x⦌ C ⦋ A / x⦌ D
11 7 10 eqtrd ⊢ A ∈ V → ⦋ A / x⦌ C C D = ⦋ A / x⦌ C ⦋ A / x⦌ C ⦋ A / x⦌ D
12 csbconstg ⊢ A ∈ V → ⦋ A / x⦌ ∅ = ∅
13 6 11 12 ifbieq12d ⊢ A ∈ V → if [˙A / x]˙ C ∈ V ∧ D ∈ V ⦋ A / x⦌ C C D ⦋ A / x⦌ ∅ = if ⦋ A / x⦌ C ∈ V ∧ ⦋ A / x⦌ D ∈ V ⦋ A / x⦌ C ⦋ A / x⦌ C ⦋ A / x⦌ D ∅
14 1 13 eqtrid ⊢ A ∈ V → ⦋ A / x⦌ if C ∈ V ∧ D ∈ V C C D ∅ = if ⦋ A / x⦌ C ∈ V ∧ ⦋ A / x⦌ D ∈ V ⦋ A / x⦌ C ⦋ A / x⦌ C ⦋ A / x⦌ D ∅
15 dfopif ⊢ C D = if C ∈ V ∧ D ∈ V C C D ∅
16 15 csbeq2i ⊢ ⦋ A / x⦌ C D = ⦋ A / x⦌ if C ∈ V ∧ D ∈ V C C D ∅
17 dfopif ⊢ ⦋ A / x⦌ C ⦋ A / x⦌ D = if ⦋ A / x⦌ C ∈ V ∧ ⦋ A / x⦌ D ∈ V ⦋ A / x⦌ C ⦋ A / x⦌ C ⦋ A / x⦌ D ∅
18 14 16 17 3eqtr4g ⊢ A ∈ V → ⦋ A / x⦌ C D = ⦋ A / x⦌ C ⦋ A / x⦌ D