Theorem sucidg 6389

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 866	. 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)
3		elsucg 6376	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)))
4	2, 3	mpbiri 258	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1541   ∈ wcel 2111  suc csuc 6308

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-sn 4577  df-suc 6312

This theorem is referenced by:  sucid  6390  nsuceq0  6391  trsuc  6395  sucssel  6403  ordsuc  7744  onpsssuc  7749  nlimsucg  7772  tfrlem11  8307  tfrlem13  8309  tz7.44-2  8326  omeulem1  8497  oeordi  8502  oeeulem  8516  dif1enlem  9069  rexdif1en  9070  dif1en  9071  php4  9119  wofib  9431  suc11reg  9509  cantnfle  9561  cantnflt2  9563  cantnfp1lem3  9570  cantnflem1  9579  dfac12lem1  10035  dfac12lem2  10036  ttukeylem3  10402  ttukeylem7  10406  r1wunlim  10628  noresle  27637  nosupprefixmo  27640  noinfprefixmo  27641  fmla  35423  ex-sategoelelomsuc  35468  ontgval  36471  sucneqond  37405  finxpreclem4  37434  finxpsuclem  37437  onexgt  43279  onepsuc  43291  ordnexbtwnsuc  43306  nlimsuc  43480  sucomisnotcard  43583