Theorem difsnpss

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

	Ref	Expression
Assertion	difsnpss	⊢ ( 𝐴 ∈ 𝐵 ↔ ( 𝐵 ∖ { 𝐴 } ) ⊊ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		notnotb	⊢ ( 𝐴 ∈ 𝐵 ↔ ¬ ¬ 𝐴 ∈ 𝐵 )
2		difss	⊢ ( 𝐵 ∖ { 𝐴 } ) ⊆ 𝐵
3	2	biantrur	⊢ ( ( 𝐵 ∖ { 𝐴 } ) ≠ 𝐵 ↔ ( ( 𝐵 ∖ { 𝐴 } ) ⊆ 𝐵 ∧ ( 𝐵 ∖ { 𝐴 } ) ≠ 𝐵 ) )
4		difsnb	⊢ ( ¬ 𝐴 ∈ 𝐵 ↔ ( 𝐵 ∖ { 𝐴 } ) = 𝐵 )
5	4	necon3bbii	⊢ ( ¬ ¬ 𝐴 ∈ 𝐵 ↔ ( 𝐵 ∖ { 𝐴 } ) ≠ 𝐵 )
6		df-pss	⊢ ( ( 𝐵 ∖ { 𝐴 } ) ⊊ 𝐵 ↔ ( ( 𝐵 ∖ { 𝐴 } ) ⊆ 𝐵 ∧ ( 𝐵 ∖ { 𝐴 } ) ≠ 𝐵 ) )
7	3 5 6	3bitr4i	⊢ ( ¬ ¬ 𝐴 ∈ 𝐵 ↔ ( 𝐵 ∖ { 𝐴 } ) ⊊ 𝐵 )
8	1 7	bitri	⊢ ( 𝐴 ∈ 𝐵 ↔ ( 𝐵 ∖ { 𝐴 } ) ⊊ 𝐵 )