Theorem sucidg 6435

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-sn 4602  df-suc 6358

This theorem is referenced by:  sucid  6436  nsuceq0  6437  trsuc  6441  sucssel  6449  ordsuc  7807  ordsucOLD  7808  onpsssuc  7813  nlimsucg  7837  tfrlem11  8402  tfrlem13  8404  tz7.44-2  8421  omeulem1  8594  oeordi  8599  oeeulem  8613  dif1enlem  9170  dif1enlemOLD  9171  rexdif1en  9172  rexdif1enOLD  9173  dif1en  9174  dif1enOLD  9176  php4  9224  wofib  9559  suc11reg  9633  cantnfle  9685  cantnflt2  9687  cantnfp1lem3  9694  cantnflem1  9703  dfac12lem1  10158  dfac12lem2  10159  ttukeylem3  10525  ttukeylem7  10529  r1wunlim  10751  noresle  27661  nosupprefixmo  27664  noinfprefixmo  27665  fmla  35403  ex-sategoelelomsuc  35448  ontgval  36449  sucneqond  37383  finxpreclem4  37412  finxpsuclem  37415  onexgt  43264  onepsuc  43276  ordnexbtwnsuc  43291  nlimsuc  43465  sucomisnotcard  43568