Theorem sucidg 6441

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

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

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 4592  df-suc 6363

This theorem is referenced by:  sucid  6442  nsuceq0  6443  trsuc  6447  sucssel  6455  ordsuc  7806  onpsssuc  7811  nlimsucg  7834  peano3  7883  tfrlem11  8371  tfrlem13  8373  tz7.44-2  8390  omeulem1  8563  oeordi  8569  oeeulem  8583  dif1enlem  9140  rexdif1en  9141  dif1en  9142  php4  9190  wofib  9503  suc11reg  9584  cantnfle  9636  cantnflt2  9638  cantnfp1lem3  9645  cantnflem1  9654  dfac12lem1  10123  dfac12lem2  10124  ttukeylem3  10491  ttukeylem7  10495  r1wunlim  10718  noresle  27823  nosupprefixmo  27826  noinfprefixmo  27827  fmla  35768  ex-sategoelelomsuc  35813  ontgval  36827  sucneqond  37894  finxpreclem4  37923  finxpsuclem  37926  dfsuccl4  39008  suceldisj  39352  onexgt  43852  onepsuc  43864  ordnexbtwnsuc  43879  nlimsuc  44052  sucomisnotcard  44155