Metamath Proof Explorer

Theorem grothprimlem

Description: Lemma for grothprim . Expand the membership of an unordered pair into primitives. (Contributed by NM, 29-Mar-2007)

Ref Expression
Assertion grothprimlem ⊢ u v ∈ w ↔ ∃ g g ∈ w ∧ ∀ h h ∈ g ↔ h = u ∨ h = v

Proof

Step Hyp Ref Expression
1 dfpr2 ⊢ u v = h | h = u ∨ h = v
2 1 eleq1i ⊢ u v ∈ w ↔ h | h = u ∨ h = v ∈ w
3 clabel ⊢ h | h = u ∨ h = v ∈ w ↔ ∃ g g ∈ w ∧ ∀ h h ∈ g ↔ h = u ∨ h = v
4 2 3 bitri ⊢ u v ∈ w ↔ ∃ g g ∈ w ∧ ∀ h h ∈ g ↔ h = u ∨ h = v