This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )