Theorem sucidg 6445

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 2769	. . 3 ⊢ 𝐴 = 𝐴
2	1	olci 879	. 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)
3		elsucg 6432	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)))
4	2, 3	mpbiri 261	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)

Syntax hints:   → wi 4   ∨ wo 860   = wceq 1567   ∈ wcel 2149  suc csuc 6363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-sn 4595  df-suc 6367

This theorem is referenced by:  sucid  6446  nsuceq0  6447  trsuc  6451  sucssel  6459  ordsuc  7810  onpsssuc  7815  nlimsucg  7838  peano3  7887  tfrlem11  8375  tfrlem13  8377  tz7.44-2  8394  omeulem1  8567  oeordi  8573  oeeulem  8587  dif1enlem  9144  rexdif1en  9145  dif1en  9146  php4  9194  wofib  9507  suc11reg  9588  cantnfle  9640  cantnflt2  9642  cantnfp1lem3  9649  cantnflem1  9658  dfac12lem1  10127  dfac12lem2  10128  ttukeylem3  10495  ttukeylem7  10499  r1wunlim  10722  noresle  27827  nosupprefixmo  27830  noinfprefixmo  27831  fmla  35772  ex-sategoelelomsuc  35817  ontgval  36831  sucneqond  37899  finxpreclem4  37928  finxpsuclem  37931  dfsuccl4  39013  suceldisj  39357  onexgt  43859  onepsuc  43871  ordnexbtwnsuc  43886  nlimsuc  44059  sucomisnotcard  44162