Theorem sucidg 6269

Description: Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). (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 2736	. . 3 ⊢ 𝐴 = 𝐴
2	1	olci 866	. 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)
3		elsucg 6258	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)))
4	2, 3	mpbiri 261	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1543   ∈ wcel 2112  suc csuc 6193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-un 3858  df-sn 4528  df-suc 6197

This theorem is referenced by:  sucid  6270  nsuceq0  6271  trsuc  6275  sucssel  6283  ordsuc  7571  onpsssuc  7576  nlimsucg  7599  tfrlem11  8102  tfrlem13  8104  tz7.44-2  8121  omeulem1  8288  oeordi  8293  oeeulem  8307  php4  8811  dif1enlem  8816  rexdif1en  8817  dif1en  8818  wofib  9139  suc11reg  9212  cantnfle  9264  cantnflt2  9266  cantnfp1lem3  9273  cantnflem1  9282  dfac12lem1  9722  dfac12lem2  9723  ttukeylem3  10090  ttukeylem7  10094  r1wunlim  10316  fmla  33010  ex-sategoelelomsuc  33055  noresle  33586  nosupprefixmo  33589  noinfprefixmo  33590  ontgval  34306  sucneqond  35222  finxpreclem4  35251  finxpsuclem  35254