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

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

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 3432  df-un 3895  df-sn 4569  df-suc 6323

This theorem is referenced by:  sucid  6401  nsuceq0  6402  trsuc  6406  sucssel  6414  ordsuc  7758  onpsssuc  7763  nlimsucg  7786  tfrlem11  8320  tfrlem13  8322  tz7.44-2  8339  omeulem1  8510  oeordi  8516  oeeulem  8530  dif1enlem  9087  rexdif1en  9088  dif1en  9089  php4  9137  wofib  9453  suc11reg  9531  cantnfle  9583  cantnflt2  9585  cantnfp1lem3  9592  cantnflem1  9601  dfac12lem1  10057  dfac12lem2  10058  ttukeylem3  10424  ttukeylem7  10428  r1wunlim  10651  noresle  27675  nosupprefixmo  27678  noinfprefixmo  27679  fmla  35579  ex-sategoelelomsuc  35624  ontgval  36629  sucneqond  37695  finxpreclem4  37724  finxpsuclem  37727  dfsuccl4  38809  suceldisj  39153  onexgt  43686  onepsuc  43698  ordnexbtwnsuc  43713  nlimsuc  43886  sucomisnotcard  43989