Metamath Proof Explorer

Theorem eldif

Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994)

Ref Expression
Assertion eldif ⊢ A ∈ B ∖ C ↔ A ∈ B ∧ ¬ A ∈ C

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ B ∖ C → A ∈ V
2 elex ⊢ A ∈ B → A ∈ V
3 2 adantr ⊢ A ∈ B ∧ ¬ A ∈ C → A ∈ V
4 eleq1 ⊢ x = y → x ∈ B ↔ y ∈ B
5 eleq1 ⊢ x = y → x ∈ C ↔ y ∈ C
6 5 notbid ⊢ x = y → ¬ x ∈ C ↔ ¬ y ∈ C
7 4 6 anbi12d ⊢ x = y → x ∈ B ∧ ¬ x ∈ C ↔ y ∈ B ∧ ¬ y ∈ C
8 eleq1 ⊢ y = A → y ∈ B ↔ A ∈ B
9 eleq1 ⊢ y = A → y ∈ C ↔ A ∈ C
10 9 notbid ⊢ y = A → ¬ y ∈ C ↔ ¬ A ∈ C
11 8 10 anbi12d ⊢ y = A → y ∈ B ∧ ¬ y ∈ C ↔ A ∈ B ∧ ¬ A ∈ C
12 df-dif ⊢ B ∖ C = x | x ∈ B ∧ ¬ x ∈ C
13 7 11 12 elab2gw ⊢ A ∈ V → A ∈ B ∖ C ↔ A ∈ B ∧ ¬ A ∈ C
14 1 3 13 pm5.21nii ⊢ A ∈ B ∖ C ↔ A ∈ B ∧ ¬ A ∈ C