Theorem elopg

Description: Characterization of the elements of an ordered pair. Closed form of elop . (Contributed by BJ, 22-Jun-2019) (Avoid depending on this detail.)

	Ref	Expression
Assertion	elopg	$$⊢\left(A\in V\wedge B\in W\right)\to \left(C\in ⟨A,B⟩\leftrightarrow \left(C=\left\{A\right\}\vee C=\left\{A,B\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfopg	$$⊢\left(A\in V\wedge B\in W\right)\to ⟨A,B⟩=\left\{\left\{A\right\},\left\{A,B\right\}\right\}$$
2		eleq2	$$⊢⟨A,B⟩=\left\{\left\{A\right\},\left\{A,B\right\}\right\}\to \left(C\in ⟨A,B⟩\leftrightarrow C\in \left\{\left\{A\right\},\left\{A,B\right\}\right\}\right)$$
3		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
4		prex	$$⊢\left\{A,B\right\}\in \mathrm{V}$$
5	3 4	elpr2	$$⊢C\in \left\{\left\{A\right\},\left\{A,B\right\}\right\}\leftrightarrow \left(C=\left\{A\right\}\vee C=\left\{A,B\right\}\right)$$
6	2 5	bitrdi	$$⊢⟨A,B⟩=\left\{\left\{A\right\},\left\{A,B\right\}\right\}\to \left(C\in ⟨A,B⟩\leftrightarrow \left(C=\left\{A\right\}\vee C=\left\{A,B\right\}\right)\right)$$
7	1 6	syl	$$⊢\left(A\in V\wedge B\in W\right)\to \left(C\in ⟨A,B⟩\leftrightarrow \left(C=\left\{A\right\}\vee C=\left\{A,B\right\}\right)\right)$$