Theorem “Intersection of 𝕀 and ×”: 𝕀 B ∩ (C × D) = 𝕀 (B ∩ C ∩ D)
Proof:
  Using “Relation extensionality”:
    Subproof for `∀ x • ∀ y • x ⦗ 𝕀 B ∩ (C × D) ⦘ y ≡ x ⦗ 𝕀 (B ∩ C ∩ D) ⦘ y`:
      For any `x`, `y`:
          x ⦗ 𝕀 B ∩ (C × D) ⦘ y
        ≡⟨ “Relation intersection” ⟩
          x ⦗ 𝕀 B ⦘ y  ∧ x ⦗ (C × D) ⦘ y
        ≡⟨ “Relationship via 𝕀” ⟩
          x = y ∈ B ∧ x ⦗ (C × D) ⦘ y
        ≡⟨ “Definition of `_⦗_⦘_`”, “Membership in ×” ⟩
          x = y ∈ B ∧ x ∈ C ∧ y ∈ D
        ≡⟨ Substitution, “Replacement” ⟩
          x = y ∧ y ∈ B ∧ (z ∈ C)[z ≔ y] ∧ y ∈ D
        ≡⟨ Substitution ⟩
          x = y ∧ y ∈ B ∧ y ∈ C ∧ y ∈ D
        ≡⟨ “Intersection” ⟩
          x = y ∧ y ∈ B ∩ C ∩ D
        ≡⟨ “Relationship via 𝕀” ⟩
          x ⦗ 𝕀 (B ∩ C ∩ D) ⦘ y


Theorem “Difference of 𝕀 and ×”: 𝕀 B - (C × D) = 𝕀 (B - (C ∩ D))
Proof:
  Using “Relation extensionality”:
    Subproof for `∀ x • ∀ y • x ⦗ 𝕀 B - (C × D) ⦘ y ≡ x ⦗ 𝕀 (B - (C ∩ D)) ⦘ y`:
      For any `x`, `y`:
          x ⦗  𝕀 B - (C × D) ⦘ y
        ≡⟨ “Relation difference” ⟩
          x ⦗ 𝕀 B ⦘ y  ∧ ¬ (x ⦗ (C × D) ⦘ y)
        ≡⟨ “Relationship via 𝕀”, “Definition of `_⦗_⦘_`”, “Membership in ×” ⟩
          x = y ∧ y ∈ B ∧ ¬ (x ∈ C ∧ y ∈ D)
        ≡⟨ “De Morgan”, “Complement” ⟩
          (x = y ∧ y ∈ B) ∧ (x ∈ ~ C ∨ y ∈ ~ D)
        ≡⟨ “Distributivity of ∧ over ∨” ⟩
          (x = y ∧ y ∈ B ∧ x ∈ ~ C) ∨ (x = y ∧ y ∈ B ∧ y ∈ ~ D)
        ≡⟨ Substitution, “Replacement” ⟩
          (x = y ∧ y ∈ B ∧ (z ∈ ~ C)[z ≔ y]) ∨ (x = y ∧ y ∈ B ∧ y ∈ ~ D)
        ≡⟨ Substitution ⟩
          (x = y ∧ y ∈ B ∧ (y ∈ ~ C)) ∨ (x = y ∧ y ∈ B ∧ y ∈ ~ D)
        ≡⟨ “Distributivity of ∧ over ∨” ⟩
          (x = y ∧ y ∈ B) ∧ (y ∈ ~ C ∨ y ∈ ~ D)
        ≡⟨ “Complement”, “De Morgan” ⟩
          (x = y ∧ y ∈ B) ∧ ¬ (y ∈ C ∧ y ∈ D)
        ≡⟨ “Intersection” ⟩
          x = y ∧ y ∈ B ∧ ¬ (y ∈ C ∩ D)
        ≡⟨ “Set difference” ⟩
          x = y ∧ y ∈ B - (C ∩ D)
        ≡⟨ “Relationship via 𝕀” ⟩
          x ⦗ 𝕀 (B - (C ∩ D)) ⦘ y