Theorem sucidg 6467

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1537   ∈ wcel 2106  suc csuc 6388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-sn 4632  df-suc 6392

This theorem is referenced by:  sucid  6468  nsuceq0  6469  trsuc  6473  sucssel  6481  ordsuc  7833  ordsucOLD  7834  onpsssuc  7839  nlimsucg  7863  tfrlem11  8427  tfrlem13  8429  tz7.44-2  8446  omeulem1  8619  oeordi  8624  oeeulem  8638  dif1enlem  9195  dif1enlemOLD  9196  rexdif1en  9197  rexdif1enOLD  9198  dif1en  9199  dif1enOLD  9201  php4  9248  wofib  9583  suc11reg  9657  cantnfle  9709  cantnflt2  9711  cantnfp1lem3  9718  cantnflem1  9727  dfac12lem1  10182  dfac12lem2  10183  ttukeylem3  10549  ttukeylem7  10553  r1wunlim  10775  noresle  27757  nosupprefixmo  27760  noinfprefixmo  27761  fmla  35366  ex-sategoelelomsuc  35411  ontgval  36414  sucneqond  37348  finxpreclem4  37377  finxpsuclem  37380  onexgt  43229  onepsuc  43241  ordnexbtwnsuc  43257  nlimsuc  43431  sucomisnotcard  43534