Theorem sucidg 6401

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

Syntax hints:   → wi 4   ∨ wo 848   = wceq 1542   ∈ wcel 2114  suc csuc 6320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-un 3907  df-sn 4582  df-suc 6324

This theorem is referenced by:  sucid  6402  nsuceq0  6403  trsuc  6407  sucssel  6415  ordsuc  7758  onpsssuc  7763  nlimsucg  7786  tfrlem11  8321  tfrlem13  8323  tz7.44-2  8340  omeulem1  8511  oeordi  8517  oeeulem  8531  dif1enlem  9088  rexdif1en  9089  dif1en  9090  php4  9138  wofib  9454  suc11reg  9532  cantnfle  9584  cantnflt2  9586  cantnfp1lem3  9593  cantnflem1  9602  dfac12lem1  10058  dfac12lem2  10059  ttukeylem3  10425  ttukeylem7  10429  r1wunlim  10652  noresle  27669  nosupprefixmo  27672  noinfprefixmo  27673  fmla  35556  ex-sategoelelomsuc  35601  ontgval  36606  sucneqond  37541  finxpreclem4  37570  finxpsuclem  37573  dfsuccl4  38646  suceldisj  38990  onexgt  43518  onepsuc  43530  ordnexbtwnsuc  43545  nlimsuc  43718  sucomisnotcard  43821