Theorem dfpr2

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

	Ref	Expression
Assertion	dfpr2	⊢ { 𝐴 , 𝐵 } = { 𝑥 ∣ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) }

Proof

Step	Hyp	Ref	Expression
1		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
2		elun	⊢ ( 𝑥 ∈ ( { 𝐴 } ∪ { 𝐵 } ) ↔ ( 𝑥 ∈ { 𝐴 } ∨ 𝑥 ∈ { 𝐵 } ) )
3		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
4		velsn	⊢ ( 𝑥 ∈ { 𝐵 } ↔ 𝑥 = 𝐵 )
5	3 4	orbi12i	⊢ ( ( 𝑥 ∈ { 𝐴 } ∨ 𝑥 ∈ { 𝐵 } ) ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) )
6	2 5	bitri	⊢ ( 𝑥 ∈ ( { 𝐴 } ∪ { 𝐵 } ) ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) )
7	6	abbi2i	⊢ ( { 𝐴 } ∪ { 𝐵 } ) = { 𝑥 ∣ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) }
8	1 7	eqtri	⊢ { 𝐴 , 𝐵 } = { 𝑥 ∣ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) }