Theorem elop

Description: Characterization of the elements of an ordered pair. Exercise 3 of TakeutiZaring p. 15. (Contributed by NM, 15-Jul-1993) (Revised by Mario Carneiro, 26-Apr-2015) Remove an extraneous hypothesis. (Revised by BJ, 25-Dec-2020) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	elop.1	$$⊢B\in \mathrm{V}$$
	elop.2	$$⊢C\in \mathrm{V}$$
Assertion	elop	$$⊢A\in ⟨B,C⟩\leftrightarrow \left(A=\left\{B\right\}\vee A=\left\{B,C\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		elop.1	$$⊢B\in \mathrm{V}$$
2		elop.2	$$⊢C\in \mathrm{V}$$
3		elopg	$$⊢\left(B\in \mathrm{V}\wedge C\in \mathrm{V}\right)\to \left(A\in ⟨B,C⟩\leftrightarrow \left(A=\left\{B\right\}\vee A=\left\{B,C\right\}\right)\right)$$
4	1 2 3	mp2an	$$⊢A\in ⟨B,C⟩\leftrightarrow \left(A=\left\{B\right\}\vee A=\left\{B,C\right\}\right)$$