Theorem difsnb

Description: ( B \ { A } ) equals B if and only if A is not a member of B . Generalization of difsn . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Assertion	difsnb	⊢ ( ¬ 𝐴 ∈ 𝐵 ↔ ( 𝐵 ∖ { 𝐴 } ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		difsn	⊢ ( ¬ 𝐴 ∈ 𝐵 → ( 𝐵 ∖ { 𝐴 } ) = 𝐵 )
2		neldifsnd	⊢ ( 𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ ( 𝐵 ∖ { 𝐴 } ) )
3		nelne1	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ ( 𝐵 ∖ { 𝐴 } ) ) → 𝐵 ≠ ( 𝐵 ∖ { 𝐴 } ) )
4	2 3	mpdan	⊢ ( 𝐴 ∈ 𝐵 → 𝐵 ≠ ( 𝐵 ∖ { 𝐴 } ) )
5	4	necomd	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐵 ∖ { 𝐴 } ) ≠ 𝐵 )
6	5	necon2bi	⊢ ( ( 𝐵 ∖ { 𝐴 } ) = 𝐵 → ¬ 𝐴 ∈ 𝐵 )
7	1 6	impbii	⊢ ( ¬ 𝐴 ∈ 𝐵 ↔ ( 𝐵 ∖ { 𝐴 } ) = 𝐵 )