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

Syntax hints:   → wi 4   ∨ wo 845   = wceq 1541   ∈ wcel 2106  suc csuc 6366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-sn 4629  df-suc 6370

This theorem is referenced by:  sucid  6446  nsuceq0  6447  trsuc  6451  sucssel  6459  ordsuc  7803  ordsucOLD  7804  onpsssuc  7809  nlimsucg  7833  tfrlem11  8390  tfrlem13  8392  tz7.44-2  8409  omeulem1  8584  oeordi  8589  oeeulem  8603  dif1enlem  9158  dif1enlemOLD  9159  rexdif1en  9160  rexdif1enOLD  9161  dif1en  9162  dif1enOLD  9164  php4  9215  wofib  9542  suc11reg  9616  cantnfle  9668  cantnflt2  9670  cantnfp1lem3  9677  cantnflem1  9686  dfac12lem1  10140  dfac12lem2  10141  ttukeylem3  10508  ttukeylem7  10512  r1wunlim  10734  noresle  27424  nosupprefixmo  27427  noinfprefixmo  27428  fmla  34658  ex-sategoelelomsuc  34703  ontgval  35619  sucneqond  36549  finxpreclem4  36578  finxpsuclem  36581  onexgt  42291  onepsuc  42303  ordnexbtwnsuc  42319  nlimsuc  42494  sucomisnotcard  42597