Description: Characterization of the elements of an ordered pair. Exercise 3 of TakeutiZaring p. 15. (Contributed by NM, 15-Jul-1993) (Revised by Mario Carneiro, 26-Apr-2015) Remove an extraneous hypothesis. (Revised by BJ, 25-Dec-2020) (Avoid depending on this detail.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | elop.1 | |- B e. _V |
|
| elop.2 | |- C e. _V |
||
| Assertion | elop | |- ( A e. <. B , C >. <-> ( A = { B } \/ A = { B , C } ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elop.1 | |- B e. _V |
|
| 2 | elop.2 | |- C e. _V |
|
| 3 | elopg | |- ( ( B e. _V /\ C e. _V ) -> ( A e. <. B , C >. <-> ( A = { B } \/ A = { B , C } ) ) ) |
|
| 4 | 1 2 3 | mp2an | |- ( A e. <. B , C >. <-> ( A = { B } \/ A = { B , C } ) ) |