Theorem difprsnss

Description: Removal of a singleton from an unordered pair. (Contributed by NM, 16-Mar-2006) (Proof shortened by Andrew Salmon, 29-Jun-2011)

	Ref	Expression
Assertion	difprsnss	⊢ ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) ⊆ { 𝐵 }

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	elpr	⊢ ( 𝑥 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) )
3		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
4	3	notbii	⊢ ( ¬ 𝑥 ∈ { 𝐴 } ↔ ¬ 𝑥 = 𝐴 )
5		biorf	⊢ ( ¬ 𝑥 = 𝐴 → ( 𝑥 = 𝐵 ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ) )
6	5	biimparc	⊢ ( ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥 = 𝐵 )
7	2 4 6	syl2anb	⊢ ( ( 𝑥 ∈ { 𝐴 , 𝐵 } ∧ ¬ 𝑥 ∈ { 𝐴 } ) → 𝑥 = 𝐵 )
8		eldif	⊢ ( 𝑥 ∈ ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) ↔ ( 𝑥 ∈ { 𝐴 , 𝐵 } ∧ ¬ 𝑥 ∈ { 𝐴 } ) )
9		velsn	⊢ ( 𝑥 ∈ { 𝐵 } ↔ 𝑥 = 𝐵 )
10	7 8 9	3imtr4i	⊢ ( 𝑥 ∈ ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) → 𝑥 ∈ { 𝐵 } )
11	10	ssriv	⊢ ( { 𝐴 , 𝐵 } ∖ { 𝐴 } ) ⊆ { 𝐵 }