Theorem sucidg 6476

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 2740	. . 3 ⊢ 𝐴 = 𝐴
2	1	olci 865	. 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)
3		elsucg 6463	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)))
4	2, 3	mpbiri 258	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)

Syntax hints:   → wi 4   ∨ wo 846   = wceq 1537   ∈ wcel 2108  suc csuc 6397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-suc 6401

This theorem is referenced by:  sucid  6477  nsuceq0  6478  trsuc  6482  sucssel  6490  ordsuc  7849  ordsucOLD  7850  onpsssuc  7855  nlimsucg  7879  tfrlem11  8444  tfrlem13  8446  tz7.44-2  8463  omeulem1  8638  oeordi  8643  oeeulem  8657  dif1enlem  9222  dif1enlemOLD  9223  rexdif1en  9224  rexdif1enOLD  9225  dif1en  9226  dif1enOLD  9228  php4  9276  wofib  9614  suc11reg  9688  cantnfle  9740  cantnflt2  9742  cantnfp1lem3  9749  cantnflem1  9758  dfac12lem1  10213  dfac12lem2  10214  ttukeylem3  10580  ttukeylem7  10584  r1wunlim  10806  noresle  27760  nosupprefixmo  27763  noinfprefixmo  27764  fmla  35349  ex-sategoelelomsuc  35394  ontgval  36397  sucneqond  37331  finxpreclem4  37360  finxpsuclem  37363  onexgt  43201  onepsuc  43213  ordnexbtwnsuc  43229  nlimsuc  43403  sucomisnotcard  43506