Theorem sucidg 6448

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1570   ∈ wcel 2146  suc csuc 6366

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-sn 4592  df-suc 6370

This theorem is used by:  sucid  6449  nsuceq0  6450  trsuc  6454  sucssel  6462  ordsuc  7812  onpsssuc  7817  nlimsucg  7840  peano3  7889  tfrlem11  8377  tfrlem13  8379  tz7.44-2  8396  omeulem1  8569  oeordi  8575  oeeulem  8589  dif1enlem  9147  rexdif1en  9148  dif1en  9149  php4  9197  wofib  9510  suc11reg  9591  cantnfle  9643  cantnflt2  9645  cantnfp1lem3  9652  cantnflem1  9661  dfac12lem1  10139  dfac12lem2  10140  ttukeylem3  10506  ttukeylem7  10510  r1wunlim  10733  noresle  27890  nosupprefixmo  27893  noinfprefixmo  27894  fmla  35886  ex-sategoelelomsuc  35931  ontgval  36975  sucneqond  38044  finxpreclem4  38073  finxpsuclem  38076  dfsuccl4  39156  suceldisj  39500  onexgt  44000  onepsuc  44012  ordnexbtwnsuc  44027  nlimsuc  44200  sucomisnotcard  44303