Description: Part of Proposition 7.23 of TakeutiZaring p. 41 (generalized). (Contributed by NM, 25-Mar-1995) (Proof shortened by Scott Fenton, 20-Feb-2012)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sucidg | |- ( A e. V -> A e. suc A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid | |- A = A |
|
| 2 | 1 | olci | |- ( A e. A \/ A = A ) |
| 3 | elsucg | |- ( A e. V -> ( A e. suc A <-> ( A e. A \/ A = A ) ) ) |
|
| 4 | 2 3 | mpbiri | |- ( A e. V -> A e. suc A ) |