Theorem elprg

Description: A member of a pair of classes is one or the other of them, and conversely as soon as it is a set. Exercise 1 of TakeutiZaring p. 15, generalized. (Contributed by NM, 13-Sep-1995)

	Ref	Expression
Assertion	elprg	$$⊢A\in V\to \left(A\in \left\{B,C\right\}\leftrightarrow \left(A=B\vee A=C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢x=A\to \left(x=B\leftrightarrow A=B\right)$$
2		eqeq1	$$⊢x=A\to \left(x=C\leftrightarrow A=C\right)$$
3	1 2	orbi12d	$$⊢x=A\to \left(\left(x=B\vee x=C\right)\leftrightarrow \left(A=B\vee A=C\right)\right)$$
4		dfpr2	$$⊢\left\{B,C\right\}=\left\{x|\left(x=B\vee x=C\right)\right\}$$
5	3 4	elab2g	$$⊢A\in V\to \left(A\in \left\{B,C\right\}\leftrightarrow \left(A=B\vee A=C\right)\right)$$