Theorem sucidg 6415

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1540   ∈ wcel 2109  suc csuc 6334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-sn 4590  df-suc 6338

This theorem is referenced by:  sucid  6416  nsuceq0  6417  trsuc  6421  sucssel  6429  ordsuc  7788  ordsucOLD  7789  onpsssuc  7794  nlimsucg  7818  tfrlem11  8356  tfrlem13  8358  tz7.44-2  8375  omeulem1  8546  oeordi  8551  oeeulem  8565  dif1enlem  9120  dif1enlemOLD  9121  rexdif1en  9122  rexdif1enOLD  9123  dif1en  9124  dif1enOLD  9126  php4  9174  wofib  9498  suc11reg  9572  cantnfle  9624  cantnflt2  9626  cantnfp1lem3  9633  cantnflem1  9642  dfac12lem1  10097  dfac12lem2  10098  ttukeylem3  10464  ttukeylem7  10468  r1wunlim  10690  noresle  27609  nosupprefixmo  27612  noinfprefixmo  27613  fmla  35368  ex-sategoelelomsuc  35413  ontgval  36419  sucneqond  37353  finxpreclem4  37382  finxpsuclem  37385  onexgt  43229  onepsuc  43241  ordnexbtwnsuc  43256  nlimsuc  43430  sucomisnotcard  43533