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	$$⊢\left\{u,v\right\}\in w\leftrightarrow \exists g\left(g\in w\wedge \forall h\left(h\in g\leftrightarrow \left(h=u\vee h=v\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfpr2	$$⊢\left\{u,v\right\}=\left\{h|\left(h=u\vee h=v\right)\right\}$$
2	1	eleq1i	$$⊢\left\{u,v\right\}\in w\leftrightarrow \left\{h|\left(h=u\vee h=v\right)\right\}\in w$$
3		clabel	$$⊢\left\{h|\left(h=u\vee h=v\right)\right\}\in w\leftrightarrow \exists g\left(g\in w\wedge \forall h\left(h\in g\leftrightarrow \left(h=u\vee h=v\right)\right)\right)$$
4	2 3	bitri	$$⊢\left\{u,v\right\}\in w\leftrightarrow \exists g\left(g\in w\wedge \forall h\left(h\in g\leftrightarrow \left(h=u\vee h=v\right)\right)\right)$$