This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eldif

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

Ref Expression
Assertion eldif ( 𝐴 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐴 ∈ ( 𝐵 ∖ 𝐶 ) → 𝐴 ∈ V )
2 elex ⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ V )
3 2 adantr ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) → 𝐴 ∈ V )
4 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
5 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶 ) )
6 5 notbid ⊢ ( 𝑥 = 𝐴 → ( ¬ 𝑥 ∈ 𝐶 ↔ ¬ 𝐴 ∈ 𝐶 ) )
7 4 6 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) ) )
8 df-dif ⊢ ( 𝐵 ∖ 𝐶 ) = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) }
9 7 8 elab2g ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) ) )
10 1 3 9 pm5.21nii ⊢ ( 𝐴 ∈ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶 ) )