Theorem sucidg 6397

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1541   ∈ wcel 2113  suc csuc 6316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-sn 4578  df-suc 6320

This theorem is referenced by:  sucid  6398  nsuceq0  6399  trsuc  6403  sucssel  6411  ordsuc  7753  onpsssuc  7758  nlimsucg  7781  tfrlem11  8316  tfrlem13  8318  tz7.44-2  8335  omeulem1  8506  oeordi  8511  oeeulem  8525  dif1enlem  9080  rexdif1en  9081  dif1en  9082  php4  9130  wofib  9442  suc11reg  9520  cantnfle  9572  cantnflt2  9574  cantnfp1lem3  9581  cantnflem1  9590  dfac12lem1  10046  dfac12lem2  10047  ttukeylem3  10413  ttukeylem7  10417  r1wunlim  10639  noresle  27656  nosupprefixmo  27659  noinfprefixmo  27660  fmla  35497  ex-sategoelelomsuc  35542  ontgval  36547  sucneqond  37482  finxpreclem4  37511  finxpsuclem  37514  dfsuccl4  38560  onexgt  43397  onepsuc  43409  ordnexbtwnsuc  43424  nlimsuc  43598  sucomisnotcard  43701