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 e. V -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 | |- ( x = y -> ( x = B <-> y = B ) ) |
|
2 | eqeq1 | |- ( x = y -> ( x = C <-> y = C ) ) |
|
3 | 1 2 | orbi12d | |- ( x = y -> ( ( x = B \/ x = C ) <-> ( y = B \/ y = C ) ) ) |
4 | eqeq1 | |- ( y = A -> ( y = B <-> A = B ) ) |
|
5 | eqeq1 | |- ( y = A -> ( y = C <-> A = C ) ) |
|
6 | 4 5 | orbi12d | |- ( y = A -> ( ( y = B \/ y = C ) <-> ( A = B \/ A = C ) ) ) |
7 | dfpr2 | |- { B , C } = { x | ( x = B \/ x = C ) } |
|
8 | 3 6 7 | elab2gw | |- ( A e. V -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) ) |