Theorem sucidg 5803

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.)

Assertion

Ref	Expression
sucidg	⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)

Proof of Theorem sucidg

Step	Hyp	Ref	Expression
1		eqid 2622	. . 3 ⊢ 𝐴 = 𝐴
2	1	olci 406	. 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)
3		elsucg 5792	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)))
4	2, 3	mpbiri 248	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)

Syntax hints:   → wi 4   ∨ wo 383   = wceq 1483   ∈ wcel 1990  suc csuc 5725

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-suc 5729

This theorem is referenced by:  sucid  5804  nsuceq0  5805  trsuc  5810  sucssel  5819  ordsuc  7014  onpsssuc  7019  nlimsucg  7042  tfrlem11  7484  tfrlem13  7486  tz7.44-2  7503  omeulem1  7662  oeordi  7667  oeeulem  7681  php4  8147  wofib  8450  suc11reg  8516  cantnfle  8568  cantnflt2  8570  cantnfp1lem3  8577  cantnflem1  8586  dfac12lem1  8965  dfac12lem2  8966  ttukeylem3  9333  ttukeylem7  9337  r1wunlim  9559  noresle  31846  noprefixmo  31848  ontgval  32430  sucneqond  33213  finxpreclem4  33231  finxpsuclem  33234