Theorem sucidg 6394

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-sn 4580  df-suc 6317

This theorem is referenced by:  sucid  6395  nsuceq0  6396  trsuc  6400  sucssel  6408  ordsuc  7752  ordsucOLD  7753  onpsssuc  7758  nlimsucg  7782  tfrlem11  8317  tfrlem13  8319  tz7.44-2  8336  omeulem1  8507  oeordi  8512  oeeulem  8526  dif1enlem  9080  dif1enlemOLD  9081  rexdif1en  9082  rexdif1enOLD  9083  dif1en  9084  dif1enOLD  9086  php4  9134  wofib  9456  suc11reg  9534  cantnfle  9586  cantnflt2  9588  cantnfp1lem3  9595  cantnflem1  9604  dfac12lem1  10057  dfac12lem2  10058  ttukeylem3  10424  ttukeylem7  10428  r1wunlim  10650  noresle  27625  nosupprefixmo  27628  noinfprefixmo  27629  fmla  35353  ex-sategoelelomsuc  35398  ontgval  36404  sucneqond  37338  finxpreclem4  37367  finxpsuclem  37370  onexgt  43213  onepsuc  43225  ordnexbtwnsuc  43240  nlimsuc  43414  sucomisnotcard  43517