Theorem sucidg 6329

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 2738	. . 3 ⊢ 𝐴 = 𝐴
2	1	olci 862	. 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)
3		elsucg 6318	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)))
4	2, 3	mpbiri 257	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)

Syntax hints:   → wi 4   ∨ wo 843   = wceq 1539   ∈ wcel 2108  suc csuc 6253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-suc 6257

This theorem is referenced by:  sucid  6330  nsuceq0  6331  trsuc  6335  sucssel  6343  ordsuc  7636  onpsssuc  7641  nlimsucg  7664  tfrlem11  8190  tfrlem13  8192  tz7.44-2  8209  omeulem1  8375  oeordi  8380  oeeulem  8394  php4  8900  dif1enlem  8905  rexdif1en  8906  dif1en  8907  wofib  9234  suc11reg  9307  cantnfle  9359  cantnflt2  9361  cantnfp1lem3  9368  cantnflem1  9377  dfac12lem1  9830  dfac12lem2  9831  ttukeylem3  10198  ttukeylem7  10202  r1wunlim  10424  fmla  33243  ex-sategoelelomsuc  33288  noresle  33827  nosupprefixmo  33830  noinfprefixmo  33831  ontgval  34547  sucneqond  35463  finxpreclem4  35492  finxpsuclem  35495