Metamath Proof Explorer

Theorem eldifeldifsn

Description: An element of a difference set is an element of the difference with a singleton. (Contributed by AV, 2-Jan-2022)

Ref Expression
Assertion eldifeldifsn 
|- ( ( X e. A /\ Y e. ( B \ A ) ) -> Y e. ( B \ { X } ) )

Proof

Step Hyp Ref Expression
1 snssi 
 |-  ( X e. A -> { X } C_ A )
2 1 sscond 
 |-  ( X e. A -> ( B \ A ) C_ ( B \ { X } ) )
3 2 sselda 
 |-  ( ( X e. A /\ Y e. ( B \ A ) ) -> Y e. ( B \ { X } ) )