Theorem sucidg 6112

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 2780	. . 3 ⊢ 𝐴 = 𝐴
2	1	olci 853	. 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)
3		elsucg 6101	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)))
4	2, 3	mpbiri 250	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)

Syntax hints:   → wi 4   ∨ wo 834   = wceq 1508   ∈ wcel 2051  suc csuc 6036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-v 3419  df-un 3836  df-sn 4445  df-suc 6040

This theorem is referenced by:  sucid  6113  nsuceq0  6114  trsuc  6118  sucssel  6126  ordsuc  7351  onpsssuc  7356  nlimsucg  7379  tfrlem11  7834  tfrlem13  7836  tz7.44-2  7853  omeulem1  8015  oeordi  8020  oeeulem  8034  php4  8506  wofib  8810  suc11reg  8882  cantnfle  8934  cantnflt2  8936  cantnfp1lem3  8943  cantnflem1  8952  dfac12lem1  9369  dfac12lem2  9370  ttukeylem3  9737  ttukeylem7  9741  r1wunlim  9963  fmla  32231  noresle  32761  noprefixmo  32763  ontgval  33339  sucneqond  34128  finxpreclem4  34156  finxpsuclem  34159