Theorem sucidg 6400

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 2740	. . 3 ⊢ 𝐴 = 𝐴
2	1	olci 872	. 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)
3		elsucg 6387	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)))
4	2, 3	mpbiri 259	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)

Syntax hints:   → wi 4   ∨ wo 853   = wceq 1547   ∈ wcel 2119  suc csuc 6319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-sn 4563  df-suc 6323

This theorem is referenced by:  sucid  6401  nsuceq0  6402  trsuc  6406  sucssel  6414  ordsuc  7761  onpsssuc  7766  nlimsucg  7789  tfrlem11  8324  tfrlem13  8326  tz7.44-2  8343  omeulem1  8514  oeordi  8520  oeeulem  8534  dif1enlem  9091  rexdif1en  9092  dif1en  9093  php4  9141  wofib  9457  suc11reg  9538  cantnfle  9590  cantnflt2  9592  cantnfp1lem3  9599  cantnflem1  9608  dfac12lem1  10064  dfac12lem2  10065  ttukeylem3  10431  ttukeylem7  10435  r1wunlim  10658  noresle  27686  nosupprefixmo  27689  noinfprefixmo  27690  fmla  35616  ex-sategoelelomsuc  35661  ontgval  36666  sucneqond  37734  finxpreclem4  37763  finxpsuclem  37766  dfsuccl4  38848  suceldisj  39192  onexgt  43692  onepsuc  43704  ordnexbtwnsuc  43719  nlimsuc  43892  sucomisnotcard  43995