Theorem elpr2g

Description: A member of a pair of sets is one or the other of them, and conversely. Exercise 1 of TakeutiZaring p. 15. (Contributed by NM, 14-Oct-2005) Generalize from sethood hypothesis to sethood antecedent. (Revised by BJ, 25-May-2024)

	Ref	Expression
Assertion	elpr2g	|- ( ( B e. V /\ C e. W ) -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. { B , C } -> A e. _V )
2	1	a1i	|- ( ( B e. V /\ C e. W ) -> ( A e. { B , C } -> A e. _V ) )
3		elex	|- ( B e. V -> B e. _V )
4		eleq1a	|- ( B e. _V -> ( A = B -> A e. _V ) )
5	3 4	syl	|- ( B e. V -> ( A = B -> A e. _V ) )
6		elex	|- ( C e. W -> C e. _V )
7		eleq1a	|- ( C e. _V -> ( A = C -> A e. _V ) )
8	6 7	syl	|- ( C e. W -> ( A = C -> A e. _V ) )
9	5 8	jaao	|- ( ( B e. V /\ C e. W ) -> ( ( A = B \/ A = C ) -> A e. _V ) )
10		elprg	|- ( A e. _V -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) )
11	10	a1i	|- ( ( B e. V /\ C e. W ) -> ( A e. _V -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) ) )
12	2 9 11	pm5.21ndd	|- ( ( B e. V /\ C e. W ) -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) )