Theorem eltpg

Description: Members of an unordered triple of classes. (Contributed by FL, 2-Feb-2014) (Proof shortened by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Assertion	eltpg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elprg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )
2		elsng	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐷 } ↔ 𝐴 = 𝐷 ) )
3	1 2	orbi12d	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ∈ { 𝐵 , 𝐶 } ∨ 𝐴 ∈ { 𝐷 } ) ↔ ( ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ∨ 𝐴 = 𝐷 ) ) )
4		df-tp	⊢ { 𝐵 , 𝐶 , 𝐷 } = ( { 𝐵 , 𝐶 } ∪ { 𝐷 } )
5	4	eleq2i	⊢ ( 𝐴 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ 𝐴 ∈ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) )
6		elun	⊢ ( 𝐴 ∈ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ↔ ( 𝐴 ∈ { 𝐵 , 𝐶 } ∨ 𝐴 ∈ { 𝐷 } ) )
7	5 6	bitri	⊢ ( 𝐴 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ ( 𝐴 ∈ { 𝐵 , 𝐶 } ∨ 𝐴 ∈ { 𝐷 } ) )
8		df-3or	⊢ ( ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ↔ ( ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ∨ 𝐴 = 𝐷 ) )
9	3 7 8	3bitr4g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ) )