Description: Obsolete version of elex2 as of 30-Nov-2024. (Contributed by Alan Sare, 25-Sep-2011) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elex2OLD | |- ( A e. B -> E. x x e. B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq1a | |- ( A e. B -> ( x = A -> x e. B ) ) |
|
| 2 | 1 | alrimiv | |- ( A e. B -> A. x ( x = A -> x e. B ) ) |
| 3 | elisset | |- ( A e. B -> E. x x = A ) |
|
| 4 | exim | |- ( A. x ( x = A -> x e. B ) -> ( E. x x = A -> E. x x e. B ) ) |
|
| 5 | 2 3 4 | sylc | |- ( A e. B -> E. x x e. B ) |