Theorem sucidg 6344

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 2738	. . 3 ⊢ 𝐴 = 𝐴
2	1	olci 863	. 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)
3		elsucg 6333	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)))
4	2, 3	mpbiri 257	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)

Syntax hints:   → wi 4   ∨ wo 844   = wceq 1539   ∈ wcel 2106  suc csuc 6268

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-sn 4562  df-suc 6272

This theorem is referenced by:  sucid  6345  nsuceq0  6346  trsuc  6350  sucssel  6358  ordsuc  7661  onpsssuc  7666  nlimsucg  7689  tfrlem11  8219  tfrlem13  8221  tz7.44-2  8238  omeulem1  8413  oeordi  8418  oeeulem  8432  dif1enlem  8943  rexdif1en  8944  dif1en  8945  php4  8996  wofib  9304  suc11reg  9377  cantnfle  9429  cantnflt2  9431  cantnfp1lem3  9438  cantnflem1  9447  dfac12lem1  9899  dfac12lem2  9900  ttukeylem3  10267  ttukeylem7  10271  r1wunlim  10493  fmla  33343  ex-sategoelelomsuc  33388  noresle  33900  nosupprefixmo  33903  noinfprefixmo  33904  ontgval  34620  sucneqond  35536  finxpreclem4  35565  finxpsuclem  35568  nlimsuc  41048  sucomisnotcard  41151