# 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 ${⊢}\left\{{A},{B}\right\}=\left\{{x}|\left({x}={A}\vee {x}={B}\right)\right\}$

### Proof

Step Hyp Ref Expression
1 df-pr ${⊢}\left\{{A},{B}\right\}=\left\{{A}\right\}\cup \left\{{B}\right\}$
2 elun ${⊢}{x}\in \left(\left\{{A}\right\}\cup \left\{{B}\right\}\right)↔\left({x}\in \left\{{A}\right\}\vee {x}\in \left\{{B}\right\}\right)$
3 velsn ${⊢}{x}\in \left\{{A}\right\}↔{x}={A}$
4 velsn ${⊢}{x}\in \left\{{B}\right\}↔{x}={B}$
5 3 4 orbi12i ${⊢}\left({x}\in \left\{{A}\right\}\vee {x}\in \left\{{B}\right\}\right)↔\left({x}={A}\vee {x}={B}\right)$
6 2 5 bitri ${⊢}{x}\in \left(\left\{{A}\right\}\cup \left\{{B}\right\}\right)↔\left({x}={A}\vee {x}={B}\right)$
7 6 abbi2i ${⊢}\left\{{A}\right\}\cup \left\{{B}\right\}=\left\{{x}|\left({x}={A}\vee {x}={B}\right)\right\}$
8 1 7 eqtri ${⊢}\left\{{A},{B}\right\}=\left\{{x}|\left({x}={A}\vee {x}={B}\right)\right\}$