Theorem sucidg 6269

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 2821	. . 3 ⊢ 𝐴 = 𝐴
2	1	olci 862	. 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)
3		elsucg 6258	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)))
4	2, 3	mpbiri 260	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)

Syntax hints:   → wi 4   ∨ wo 843   = wceq 1537   ∈ wcel 2114  suc csuc 6193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-sn 4568  df-suc 6197

This theorem is referenced by:  sucid  6270  nsuceq0  6271  trsuc  6275  sucssel  6283  ordsuc  7529  onpsssuc  7534  nlimsucg  7557  tfrlem11  8024  tfrlem13  8026  tz7.44-2  8043  omeulem1  8208  oeordi  8213  oeeulem  8227  php4  8704  wofib  9009  suc11reg  9082  cantnfle  9134  cantnflt2  9136  cantnfp1lem3  9143  cantnflem1  9152  dfac12lem1  9569  dfac12lem2  9570  ttukeylem3  9933  ttukeylem7  9937  r1wunlim  10159  fmla  32628  ex-sategoelelomsuc  32673  noresle  33200  noprefixmo  33202  ontgval  33779  sucneqond  34649  finxpreclem4  34678  finxpsuclem  34681