Metamath Proof Explorer

Theorem neldifpr2

Description: The second element of a pair is not an element of a difference with this pair. (Contributed by Thierry Arnoux, 20-Nov-2023)

Ref Expression
Assertion neldifpr2 
|- -. B e. ( C \ { A , B } )

Proof

Step Hyp Ref Expression
1 neirr 
 |-  -. B =/= B
2 eldifpr 
 |-  ( B e. ( C \ { A , B } ) <-> ( B e. C /\ B =/= A /\ B =/= B ) )
3 2 simp3bi 
 |-  ( B e. ( C \ { A , B } ) -> B =/= B )
4 1 3 mto 
 |-  -. B e. ( C \ { A , B } )