Theorem sucidg 5944

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 2771	. . 3 ⊢ 𝐴 = 𝐴
2	1	olci 855	. 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)
3		elsucg 5933	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)))
4	2, 3	mpbiri 248	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)

Syntax hints:   → wi 4   ∨ wo 836   = wceq 1631   ∈ wcel 2145  suc csuc 5866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728  df-sn 4317  df-suc 5870

This theorem is referenced by:  sucid  5945  nsuceq0  5946  trsuc  5951  sucssel  5960  ordsuc  7159  onpsssuc  7164  nlimsucg  7187  tfrlem11  7635  tfrlem13  7637  tz7.44-2  7654  omeulem1  7814  oeordi  7819  oeeulem  7833  php4  8301  wofib  8604  suc11reg  8678  cantnfle  8730  cantnflt2  8732  cantnfp1lem3  8739  cantnflem1  8748  dfac12lem1  9165  dfac12lem2  9166  ttukeylem3  9533  ttukeylem7  9537  r1wunlim  9759  noresle  32176  noprefixmo  32178  ontgval  32760  sucneqond  33543  finxpreclem4  33561  finxpsuclem  33564