Theorem sucidg 6418

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1540   ∈ wcel 2109  suc csuc 6337

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-sn 4593  df-suc 6341

This theorem is referenced by:  sucid  6419  nsuceq0  6420  trsuc  6424  sucssel  6432  ordsuc  7791  ordsucOLD  7792  onpsssuc  7797  nlimsucg  7821  tfrlem11  8359  tfrlem13  8361  tz7.44-2  8378  omeulem1  8549  oeordi  8554  oeeulem  8568  dif1enlem  9126  dif1enlemOLD  9127  rexdif1en  9128  rexdif1enOLD  9129  dif1en  9130  dif1enOLD  9132  php4  9180  wofib  9505  suc11reg  9579  cantnfle  9631  cantnflt2  9633  cantnfp1lem3  9640  cantnflem1  9649  dfac12lem1  10104  dfac12lem2  10105  ttukeylem3  10471  ttukeylem7  10475  r1wunlim  10697  noresle  27616  nosupprefixmo  27619  noinfprefixmo  27620  fmla  35375  ex-sategoelelomsuc  35420  ontgval  36426  sucneqond  37360  finxpreclem4  37389  finxpsuclem  37392  onexgt  43236  onepsuc  43248  ordnexbtwnsuc  43263  nlimsuc  43437  sucomisnotcard  43540