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) (Proof shortened by JJ, 23-Jul-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | elpr2.1 | |- B e. _V |
|
| elpr2.2 | |- C e. _V |
||
| Assertion | elpr2 | |- ( A e. { B , C } <-> ( A = B \/ A = C ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elpr2.1 | |- B e. _V |
|
| 2 | elpr2.2 | |- C e. _V |
|
| 3 | elpr2g | |- ( ( B e. _V /\ C e. _V ) -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) ) |
|
| 4 | 1 2 3 | mp2an | |- ( A e. { B , C } <-> ( A = B \/ A = C ) ) |