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 } u. { B } )
2 elun
 |-  ( x e. ( { A } u. { B } ) <-> ( x e. { A } \/ x e. { B } ) )
3 velsn
 |-  ( x e. { A } <-> x = A )
4 velsn
 |-  ( x e. { B } <-> x = B )
5 3 4 orbi12i
 |-  ( ( x e. { A } \/ x e. { B } ) <-> ( x = A \/ x = B ) )
6 2 5 bitri
 |-  ( x e. ( { A } u. { B } ) <-> ( x = A \/ x = B ) )
7 6 abbi2i
 |-  ( { A } u. { B } ) = { x | ( x = A \/ x = B ) }
8 1 7 eqtri
 |-  { A , B } = { x | ( x = A \/ x = B ) }