Metamath Proof Explorer


Theorem dfpr2

Description: Alternate definition of a pair. Definition 5.1 of TakeutiZaring p. 15. (Contributed by NM, 24-Apr-1994)

Ref Expression
Assertion dfpr2 A B = x | x = A x = B

Proof

Step Hyp Ref Expression
1 df-pr A B = A B
2 elun x A B x A x B
3 velsn x A x = A
4 velsn x B x = B
5 3 4 orbi12i x A x B x = A x = B
6 2 5 bitri x A B x = A x = B
7 6 abbi2i A B = x | x = A x = B
8 1 7 eqtri A B = x | x = A x = B