Theorem sucidg 6341

Description: Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). (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 2739	. . 3 ⊢ 𝐴 = 𝐴
2	1	olci 862	. 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)
3		elsucg 6330	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)))
4	2, 3	mpbiri 257	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)

Syntax hints:   → wi 4   ∨ wo 843   = wceq 1541   ∈ wcel 2109  suc csuc 6265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-un 3896  df-sn 4567  df-suc 6269

This theorem is referenced by:  sucid  6342  nsuceq0  6343  trsuc  6347  sucssel  6355  ordsuc  7649  onpsssuc  7654  nlimsucg  7677  tfrlem11  8203  tfrlem13  8205  tz7.44-2  8222  omeulem1  8389  oeordi  8394  oeeulem  8408  dif1enlem  8908  rexdif1en  8909  dif1en  8910  php4  8960  wofib  9265  suc11reg  9338  cantnfle  9390  cantnflt2  9392  cantnfp1lem3  9399  cantnflem1  9408  dfac12lem1  9883  dfac12lem2  9884  ttukeylem3  10251  ttukeylem7  10255  r1wunlim  10477  fmla  33322  ex-sategoelelomsuc  33367  noresle  33879  nosupprefixmo  33882  noinfprefixmo  33883  ontgval  34599  sucneqond  35515  finxpreclem4  35544  finxpsuclem  35547