Theorem dftp2

Description: Alternate definition of unordered triple of classes. Special case of Definition 5.3 of TakeutiZaring p. 16. (Contributed by NM, 8-Apr-1994)

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

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	eltp	⊢ ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) )
3	2	eqabi	⊢ { 𝐴 , 𝐵 , 𝐶 } = { 𝑥 ∣ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) }