Theorem sucidg 6403

Description: Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). Lemma 1.7 of [Schloeder] p. 1. (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 2731	. . 3 ⊢ 𝐴 = 𝐴
2	1	olci 864	. 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)
3		elsucg 6390	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)))
4	2, 3	mpbiri 257	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)

Syntax hints:   → wi 4   ∨ wo 845   = wceq 1541   ∈ wcel 2106  suc csuc 6324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-un 3918  df-sn 4592  df-suc 6328

This theorem is referenced by:  sucid  6404  nsuceq0  6405  trsuc  6409  sucssel  6417  ordsuc  7753  ordsucOLD  7754  onpsssuc  7759  nlimsucg  7783  tfrlem11  8339  tfrlem13  8341  tz7.44-2  8358  omeulem1  8534  oeordi  8539  oeeulem  8553  dif1enlem  9107  dif1enlemOLD  9108  rexdif1en  9109  rexdif1enOLD  9110  dif1en  9111  dif1enOLD  9113  php4  9164  wofib  9490  suc11reg  9564  cantnfle  9616  cantnflt2  9618  cantnfp1lem3  9625  cantnflem1  9634  dfac12lem1  10088  dfac12lem2  10089  ttukeylem3  10456  ttukeylem7  10460  r1wunlim  10682  noresle  27082  nosupprefixmo  27085  noinfprefixmo  27086  fmla  34062  ex-sategoelelomsuc  34107  ontgval  34979  sucneqond  35909  finxpreclem4  35938  finxpsuclem  35941  onexgt  41632  onepsuc  41644  ordnexbtwnsuc  41660  nlimsuc  41835  sucomisnotcard  41938