Theorem sucidg 6446

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

Syntax hints:   → wi 4   ∨ wo 860   = wceq 1570   ∈ wcel 2143  suc csuc 6364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-sn 4591  df-suc 6368

This theorem is referenced by:  sucid  6447  nsuceq0  6448  trsuc  6452  sucssel  6460  ordsuc  7811  onpsssuc  7816  nlimsucg  7839  peano3  7888  tfrlem11  8376  tfrlem13  8378  tz7.44-2  8395  omeulem1  8568  oeordi  8574  oeeulem  8588  dif1enlem  9145  rexdif1en  9146  dif1en  9147  php4  9195  wofib  9508  suc11reg  9589  cantnfle  9641  cantnflt2  9643  cantnfp1lem3  9650  cantnflem1  9659  dfac12lem1  10128  dfac12lem2  10129  ttukeylem3  10496  ttukeylem7  10500  r1wunlim  10723  noresle  27842  nosupprefixmo  27845  noinfprefixmo  27846  fmla  35854  ex-sategoelelomsuc  35899  ontgval  36923  sucneqond  37992  finxpreclem4  38021  finxpsuclem  38024  dfsuccl4  39104  suceldisj  39448  onexgt  43950  onepsuc  43962  ordnexbtwnsuc  43977  nlimsuc  44150  sucomisnotcard  44253