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

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

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-sn 4585  df-suc 6363

This theorem is used by:  sucid  6442  nsuceq0  6443  trsuc  6447  sucssel  6455  ordsuc  7810  onpsssuc  7815  nlimsucg  7838  peano3  7887  tfrlem11  8377  tfrlem13  8379  tz7.44-2  8396  omeulem1  8569  oeordi  8575  oeeulem  8589  dif1enlem  9154  rexdif1en  9155  dif1en  9156  php4  9204  wofib  9517  suc11reg  9598  cantnfle  9650  cantnflt2  9652  cantnfp1lem3  9659  cantnflem1  9668  dfac12lem1  10146  dfac12lem2  10147  ttukeylem3  10513  ttukeylem7  10517  r1wunlim  10746  noresle  27933  nosupprefixmo  27936  noinfprefixmo  27937  fmla  35960  ex-sategoelelomsuc  36005  ontgval  37050  sucneqond  38119  finxpreclem4  38148  finxpsuclem  38151  dfsuccl4  39222  suceldisj  39566  onexgt  44081  onepsuc  44093  ordnexbtwnsuc  44108  nlimsuc  44281  sucomisnotcard  44384