Metamath Proof Explorer

Theorem dfdif3OLD

Description: Obsolete version of dfdif3 as of 15-Aug-2025. (Contributed by BJ and Jim Kingdon, 16-Jun-2022) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dfdif3OLD ⊢ A ∖ B = x ∈ A | ∀ y ∈ B x ≠ y

Proof

Step Hyp Ref Expression
1 dfdif2 ⊢ A ∖ B = x ∈ A | ¬ x ∈ B
2 ax6ev ⊢ ∃ y y = x
3 2 biantrur ⊢ ¬ x ∈ B ↔ ∃ y y = x ∧ ¬ x ∈ B
4 19.41v ⊢ ∃ y y = x ∧ ¬ x ∈ B ↔ ∃ y y = x ∧ ¬ x ∈ B
5 3 4 bitr4i ⊢ ¬ x ∈ B ↔ ∃ y y = x ∧ ¬ x ∈ B
6 sbalex ⊢ ∃ y y = x ∧ ¬ x ∈ B ↔ ∀ y y = x → ¬ x ∈ B
7 equcom ⊢ y = x ↔ x = y
8 7 imbi1i ⊢ y = x → ¬ x ∈ B ↔ x = y → ¬ x ∈ B
9 eleq1w ⊢ x = y → x ∈ B ↔ y ∈ B
10 9 notbid ⊢ x = y → ¬ x ∈ B ↔ ¬ y ∈ B
11 10 pm5.74i ⊢ x = y → ¬ x ∈ B ↔ x = y → ¬ y ∈ B
12 con2b ⊢ x = y → ¬ y ∈ B ↔ y ∈ B → ¬ x = y
13 df-ne ⊢ x ≠ y ↔ ¬ x = y
14 13 bicomi ⊢ ¬ x = y ↔ x ≠ y
15 14 imbi2i ⊢ y ∈ B → ¬ x = y ↔ y ∈ B → x ≠ y
16 11 12 15 3bitri ⊢ x = y → ¬ x ∈ B ↔ y ∈ B → x ≠ y
17 8 16 bitri ⊢ y = x → ¬ x ∈ B ↔ y ∈ B → x ≠ y
18 17 albii ⊢ ∀ y y = x → ¬ x ∈ B ↔ ∀ y y ∈ B → x ≠ y
19 5 6 18 3bitri ⊢ ¬ x ∈ B ↔ ∀ y y ∈ B → x ≠ y
20 df-ral ⊢ ∀ y ∈ B x ≠ y ↔ ∀ y y ∈ B → x ≠ y
21 19 20 bitr4i ⊢ ¬ x ∈ B ↔ ∀ y ∈ B x ≠ y
22 21 rabbii ⊢ x ∈ A | ¬ x ∈ B = x ∈ A | ∀ y ∈ B x ≠ y
23 1 22 eqtri ⊢ A ∖ B = x ∈ A | ∀ y ∈ B x ≠ y