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	⊢ ( { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfpr2	⊢ { 𝑢 , 𝑣 } = { ℎ ∣ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) }
2	1	eleq1i	⊢ ( { 𝑢 , 𝑣 } ∈ 𝑤 ↔ { ℎ ∣ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) } ∈ 𝑤 )
3		clabel	⊢ ( { ℎ ∣ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) } ∈ 𝑤 ↔ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) )
4	2 3	bitri	⊢ ( { 𝑢 , 𝑣 } ∈ 𝑤 ↔ ∃ 𝑔 ( 𝑔 ∈ 𝑤 ∧ ∀ ℎ ( ℎ ∈ 𝑔 ↔ ( ℎ = 𝑢 ∨ ℎ = 𝑣 ) ) ) )