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

Metamath Proof Explorer

Theorem el7g

Description: Members of a set with seven elements. Lemma for usgrexmpl2nb0 etc. (Contributed by AV, 9-Aug-2025)

Ref Expression
Assertion el7g ⊢ X ∈ V → X ∈ A ∪ B C D ∪ E F G ↔ X = A ∨ X = B ∨ X = C ∨ X = D ∨ X = E ∨ X = F ∨ X = G

Proof

Step Hyp Ref Expression
1 elun ⊢ X ∈ A ∪ B C D ∪ E F G ↔ X ∈ A ∨ X ∈ B C D ∪ E F G
2 elsng ⊢ X ∈ V → X ∈ A ↔ X = A
3 elun ⊢ X ∈ B C D ∪ E F G ↔ X ∈ B C D ∨ X ∈ E F G
4 eltpg ⊢ X ∈ V → X ∈ B C D ↔ X = B ∨ X = C ∨ X = D
5 eltpg ⊢ X ∈ V → X ∈ E F G ↔ X = E ∨ X = F ∨ X = G
6 4 5 orbi12d ⊢ X ∈ V → X ∈ B C D ∨ X ∈ E F G ↔ X = B ∨ X = C ∨ X = D ∨ X = E ∨ X = F ∨ X = G
7 3 6 bitrid ⊢ X ∈ V → X ∈ B C D ∪ E F G ↔ X = B ∨ X = C ∨ X = D ∨ X = E ∨ X = F ∨ X = G
8 2 7 orbi12d ⊢ X ∈ V → X ∈ A ∨ X ∈ B C D ∪ E F G ↔ X = A ∨ X = B ∨ X = C ∨ X = D ∨ X = E ∨ X = F ∨ X = G
9 1 8 bitrid ⊢ X ∈ V → X ∈ A ∪ B C D ∪ E F G ↔ X = A ∨ X = B ∨ X = C ∨ X = D ∨ X = E ∨ X = F ∨ X = G