This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqabi ⊢ A ∪ B = x | x = A ∨ x = B
8 1 7 eqtri ⊢ A B = x | x = A ∨ x = B