Metamath Proof Explorer


Theorem difprsn1

Description: Removal of a singleton from an unordered pair. (Contributed by Thierry Arnoux, 4-Feb-2017)

Ref Expression
Assertion difprsn1 A B A B A = B

Proof

Step Hyp Ref Expression
1 necom B A A B
2 disjsn2 B A B A =
3 disj3 B A = B = B A
4 2 3 sylib B A B = B A
5 df-pr A B = A B
6 5 equncomi A B = B A
7 6 difeq1i A B A = B A A
8 difun2 B A A = B A
9 7 8 eqtri A B A = B A
10 4 9 syl6reqr B A A B A = B
11 1 10 sylbir A B A B A = B