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 2760	. . 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 1569   ∈ wcel 2144  suc csuc 6366

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4150  df-sn 4585  df-suc 6370

This theorem is used by:  sucid  6449  nsuceq0  6450  trsuc  6454  sucssel  6462  ordsuc  7827  onpsssuc  7832  nlimsucg  7855  peano3  7904  tfrlem11  8401  tfrlem13  8403  tz7.44-2  8420  omeulem1  8595  oeordi  8601  oeeulem  8615  dif1enlem  9180  rexdif1en  9181  dif1en  9182  php4  9230  wofib  9544  suc11reg  9625  cantnfle  9677  cantnflt2  9679  cantnfp1lem3  9686  cantnflem1  9695  dfac12lem1  10227  dfac12lem2  10228  ttukeylem3  10594  ttukeylem7  10598  r1wunlim  10827  noresle  28061  nosupprefixmo  28064  noinfprefixmo  28065  fmla  36234  ex-sategoelelomsuc  36279  ontgval  37313  sucneqond  38395  finxpreclem4  38424  finxpsuclem  38427  dfsuccl4  39513  suceldisj  39857  onexgt  44349  onepsuc  44361  ordnexbtwnsuc  44376  nlimsuc  44549  sucomisnotcard  44652