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 2761	. . 3 ⊢ 𝐴 = 𝐴
2	1	olci 880	. 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)
3		elsucg 6432	. 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 6363

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-suc 6367

This theorem is used by:  sucid  6446  nsuceq0  6447  trsuc  6451  sucssel  6459  ordsuc  7823  onpsssuc  7828  nlimsucg  7851  peano3  7900  tfrlem11  8389  tfrlem13  8391  tz7.44-2  8408  omeulem1  8583  oeordi  8589  oeeulem  8603  dif1enlem  9168  rexdif1en  9169  dif1en  9170  php4  9218  wofib  9532  suc11reg  9613  cantnfle  9665  cantnflt2  9667  cantnfp1lem3  9674  cantnflem1  9683  dfac12lem1  10215  dfac12lem2  10216  ttukeylem3  10582  ttukeylem7  10586  r1wunlim  10815  noresle  28047  nosupprefixmo  28050  noinfprefixmo  28051  fmla  36125  ex-sategoelelomsuc  36170  ontgval  37199  sucneqond  38268  finxpreclem4  38297  finxpsuclem  38300  dfsuccl4  39386  suceldisj  39730  onexgt  44226  onepsuc  44238  ordnexbtwnsuc  44253  nlimsuc  44426  sucomisnotcard  44529