Metamath Proof Explorer

Theorem difpr

Description: Removing two elements as pair of elements corresponds to removing each of the two elements as singletons. (Contributed by Alexander van der Vekens, 13-Jul-2018)

Ref Expression
Assertion difpr A B C = A B C


Step Hyp Ref Expression
1 df-pr B C = B C
2 1 difeq2i A B C = A B C
3 difun1 A B C = A B C
4 2 3 eqtri A B C = A B C