Metamath Proof Explorer

Theorem difjust

Description: Soundness justification theorem for df-dif . (Contributed by Rodolfo Medina, 27-Apr-2010) (Proof shortened by Andrew Salmon, 9-Jul-2011)

Ref Expression
Assertion difjust ⊢ x | x ∈ A ∧ ¬ x ∈ B = y | y ∈ A ∧ ¬ y ∈ B

Proof

Step Hyp Ref Expression
1 eleq1w ⊢ x = z → x ∈ A ↔ z ∈ A
2 eleq1w ⊢ x = z → x ∈ B ↔ z ∈ B
3 2 notbid ⊢ x = z → ¬ x ∈ B ↔ ¬ z ∈ B
4 1 3 anbi12d ⊢ x = z → x ∈ A ∧ ¬ x ∈ B ↔ z ∈ A ∧ ¬ z ∈ B
5 4 cbvabv ⊢ x | x ∈ A ∧ ¬ x ∈ B = z | z ∈ A ∧ ¬ z ∈ B
6 eleq1w ⊢ z = y → z ∈ A ↔ y ∈ A
7 eleq1w ⊢ z = y → z ∈ B ↔ y ∈ B
8 7 notbid ⊢ z = y → ¬ z ∈ B ↔ ¬ y ∈ B
9 6 8 anbi12d ⊢ z = y → z ∈ A ∧ ¬ z ∈ B ↔ y ∈ A ∧ ¬ y ∈ B
10 9 cbvabv ⊢ z | z ∈ A ∧ ¬ z ∈ B = y | y ∈ A ∧ ¬ y ∈ B
11 5 10 eqtri ⊢ x | x ∈ A ∧ ¬ x ∈ B = y | y ∈ A ∧ ¬ y ∈ B