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

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ) )