Theorem ssdifsn

Description: Subset of a set with an element removed. (Contributed by Emmett Weisz, 7-Jul-2021) (Proof shortened by JJ, 31-May-2022)

	Ref	Expression
Assertion	ssdifsn	|- ( A C_ ( B \ { C } ) <-> ( A C_ B /\ -. C e. A ) )

Proof

Step	Hyp	Ref	Expression
1		difss2	|- ( A C_ ( B \ { C } ) -> A C_ B )
2		reldisj	|- ( A C_ B -> ( ( A i^i { C } ) = (/) <-> A C_ ( B \ { C } ) ) )
3	2	bicomd	|- ( A C_ B -> ( A C_ ( B \ { C } ) <-> ( A i^i { C } ) = (/) ) )
4	1 3	biadanii	|- ( A C_ ( B \ { C } ) <-> ( A C_ B /\ ( A i^i { C } ) = (/) ) )
5		disjsn	|- ( ( A i^i { C } ) = (/) <-> -. C e. A )
6	5	anbi2i	|- ( ( A C_ B /\ ( A i^i { C } ) = (/) ) <-> ( A C_ B /\ -. C e. A ) )
7	4 6	bitri	|- ( A C_ ( B \ { C } ) <-> ( A C_ B /\ -. C e. A ) )