Theorem sucidg 6424

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

Syntax hints:   → wi 4   ∨ wo 858   = wceq 1559   ∈ wcel 2141  suc csuc 6343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-sn 4580  df-suc 6347

This theorem is referenced by:  sucid  6425  nsuceq0  6426  trsuc  6430  sucssel  6438  ordsuc  7789  onpsssuc  7794  nlimsucg  7817  peano3  7866  tfrlem11  8353  tfrlem13  8355  tz7.44-2  8372  omeulem1  8545  oeordi  8551  oeeulem  8565  dif1enlem  9122  rexdif1en  9123  dif1en  9124  php4  9172  wofib  9487  suc11reg  9568  cantnfle  9620  cantnflt2  9622  cantnfp1lem3  9629  cantnflem1  9638  dfac12lem1  10094  dfac12lem2  10095  ttukeylem3  10462  ttukeylem7  10466  r1wunlim  10689  noresle  27749  nosupprefixmo  27752  noinfprefixmo  27753  fmla  35692  ex-sategoelelomsuc  35737  ontgval  36752  sucneqond  37820  finxpreclem4  37849  finxpsuclem  37852  dfsuccl4  38934  suceldisj  39278  onexgt  43778  onepsuc  43790  ordnexbtwnsuc  43805  nlimsuc  43978  sucomisnotcard  44081