| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eleq1 2829 | . . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 ∈ Cℋ
↔ 𝐴 ∈
Cℋ )) | 
| 2 | 1 | anbi1d 631 | . . . 4
⊢ (𝑥 = 𝐴 → ((𝑥 ∈ Cℋ
∧ 𝑦 ∈
Cℋ ) ↔ (𝐴 ∈ Cℋ
∧ 𝑦 ∈
Cℋ ))) | 
| 3 |  | id 22 | . . . . 5
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) | 
| 4 |  | ineq1 4213 | . . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝑦) = (𝐴 ∩ 𝑦)) | 
| 5 |  | ineq1 4213 | . . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ∩ (⊥‘𝑦)) = (𝐴 ∩ (⊥‘𝑦))) | 
| 6 | 4, 5 | oveq12d 7449 | . . . . 5
⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝑦) ∨ℋ (𝑥 ∩ (⊥‘𝑦))) = ((𝐴 ∩ 𝑦) ∨ℋ (𝐴 ∩ (⊥‘𝑦)))) | 
| 7 | 3, 6 | eqeq12d 2753 | . . . 4
⊢ (𝑥 = 𝐴 → (𝑥 = ((𝑥 ∩ 𝑦) ∨ℋ (𝑥 ∩ (⊥‘𝑦))) ↔ 𝐴 = ((𝐴 ∩ 𝑦) ∨ℋ (𝐴 ∩ (⊥‘𝑦))))) | 
| 8 | 2, 7 | anbi12d 632 | . . 3
⊢ (𝑥 = 𝐴 → (((𝑥 ∈ Cℋ
∧ 𝑦 ∈
Cℋ ) ∧ 𝑥 = ((𝑥 ∩ 𝑦) ∨ℋ (𝑥 ∩ (⊥‘𝑦)))) ↔ ((𝐴 ∈ Cℋ
∧ 𝑦 ∈
Cℋ ) ∧ 𝐴 = ((𝐴 ∩ 𝑦) ∨ℋ (𝐴 ∩ (⊥‘𝑦)))))) | 
| 9 |  | eleq1 2829 | . . . . 5
⊢ (𝑦 = 𝐵 → (𝑦 ∈ Cℋ
↔ 𝐵 ∈
Cℋ )) | 
| 10 | 9 | anbi2d 630 | . . . 4
⊢ (𝑦 = 𝐵 → ((𝐴 ∈ Cℋ
∧ 𝑦 ∈
Cℋ ) ↔ (𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ ))) | 
| 11 |  | ineq2 4214 | . . . . . 6
⊢ (𝑦 = 𝐵 → (𝐴 ∩ 𝑦) = (𝐴 ∩ 𝐵)) | 
| 12 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑦 = 𝐵 → (⊥‘𝑦) = (⊥‘𝐵)) | 
| 13 | 12 | ineq2d 4220 | . . . . . 6
⊢ (𝑦 = 𝐵 → (𝐴 ∩ (⊥‘𝑦)) = (𝐴 ∩ (⊥‘𝐵))) | 
| 14 | 11, 13 | oveq12d 7449 | . . . . 5
⊢ (𝑦 = 𝐵 → ((𝐴 ∩ 𝑦) ∨ℋ (𝐴 ∩ (⊥‘𝑦))) = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ (⊥‘𝐵)))) | 
| 15 | 14 | eqeq2d 2748 | . . . 4
⊢ (𝑦 = 𝐵 → (𝐴 = ((𝐴 ∩ 𝑦) ∨ℋ (𝐴 ∩ (⊥‘𝑦))) ↔ 𝐴 = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ (⊥‘𝐵))))) | 
| 16 | 10, 15 | anbi12d 632 | . . 3
⊢ (𝑦 = 𝐵 → (((𝐴 ∈ Cℋ
∧ 𝑦 ∈
Cℋ ) ∧ 𝐴 = ((𝐴 ∩ 𝑦) ∨ℋ (𝐴 ∩ (⊥‘𝑦)))) ↔ ((𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ ) ∧ 𝐴 = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ (⊥‘𝐵)))))) | 
| 17 |  | df-cm 31602 | . . 3
⊢ 
𝐶ℋ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ Cℋ
∧ 𝑦 ∈
Cℋ ) ∧ 𝑥 = ((𝑥 ∩ 𝑦) ∨ℋ (𝑥 ∩ (⊥‘𝑦))))} | 
| 18 | 8, 16, 17 | brabg 5544 | . 2
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝐶ℋ 𝐵 ↔ ((𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ ) ∧ 𝐴 = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ (⊥‘𝐵)))))) | 
| 19 | 18 | bianabs 541 | 1
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝐶ℋ 𝐵 ↔ 𝐴 = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ (⊥‘𝐵))))) |