Theorem sucidg 6450

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

Syntax hints:   → wi 4   ∨ wo 846   = wceq 1534   ∈ wcel 2099  suc csuc 6371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-un 3952  df-sn 4630  df-suc 6375

This theorem is referenced by:  sucid  6451  nsuceq0  6452  trsuc  6456  sucssel  6464  ordsuc  7816  ordsucOLD  7817  onpsssuc  7822  nlimsucg  7846  tfrlem11  8408  tfrlem13  8410  tz7.44-2  8427  omeulem1  8602  oeordi  8607  oeeulem  8621  dif1enlem  9180  dif1enlemOLD  9181  rexdif1en  9182  rexdif1enOLD  9183  dif1en  9184  dif1enOLD  9186  php4  9237  wofib  9568  suc11reg  9642  cantnfle  9694  cantnflt2  9696  cantnfp1lem3  9703  cantnflem1  9712  dfac12lem1  10166  dfac12lem2  10167  ttukeylem3  10534  ttukeylem7  10538  r1wunlim  10760  noresle  27629  nosupprefixmo  27632  noinfprefixmo  27633  fmla  34991  ex-sategoelelomsuc  35036  ontgval  35915  sucneqond  36844  finxpreclem4  36873  finxpsuclem  36876  onexgt  42668  onepsuc  42680  ordnexbtwnsuc  42696  nlimsuc  42871  sucomisnotcard  42974