Description: Obsolete version of elpr2 as of 25-May-2024. (Contributed by NM, 14-Oct-2005) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | elpr2.1 | |- B e. _V |
|
| elpr2.2 | |- C e. _V |
||
| Assertion | elpr2OLD | |- ( 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 | elex | |- ( A e. { B , C } -> A e. _V ) |
|
| 4 | eleq1 | |- ( A = B -> ( A e. _V <-> B e. _V ) ) |
|
| 5 | 1 4 | mpbiri | |- ( A = B -> A e. _V ) |
| 6 | eleq1 | |- ( A = C -> ( A e. _V <-> C e. _V ) ) |
|
| 7 | 2 6 | mpbiri | |- ( A = C -> A e. _V ) |
| 8 | 5 7 | jaoi | |- ( ( A = B \/ A = C ) -> A e. _V ) |
| 9 | elprg | |- ( A e. _V -> ( A e. { B , C } <-> ( A = B \/ A = C ) ) ) |
|
| 10 | 3 8 9 | pm5.21nii | |- ( A e. { B , C } <-> ( A = B \/ A = C ) ) |