Theorem sucidg 6472

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 2763	. . 3 ⊢ 𝐴 = 𝐴
2	1	olci 880	. 2 ⊢ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)
3		elsucg 6459	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴 ∈ 𝐴 ∨ 𝐴 = 𝐴)))
4	2, 3	mpbiri 261	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1570   ∈ wcel 2147  suc csuc 6390

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-suc 6394

This theorem is used by:  sucid  6473  nsuceq0  6474  trsuc  6478  sucssel  6486  ordsuc  7859  onpsssuc  7864  nlimsucg  7887  peano3  7936  tfrlem11  8434  tfrlem13  8436  tz7.44-2  8453  omeulem1  8628  oeordi  8634  oeeulem  8648  dif1enlem  9213  rexdif1en  9214  dif1en  9215  php4  9263  wofib  9576  suc11reg  9657  cantnfle  9709  cantnflt2  9711  cantnfp1lem3  9718  cantnflem1  9727  dfac12lem1  10261  dfac12lem2  10262  ttukeylem3  10628  ttukeylem7  10632  r1wunlim  10861  noresle  28111  nosupprefixmo  28114  noinfprefixmo  28115  eqsucidi  35831  8olt9o  35914  7olt9o  35915  6olt9o  35916  5olt9o  35917  4olt9o  35918  3olt9o  35919  2olt9o  35920  1olt9o  35921  fmla  36354  ex-sategoelelomsuc  36399  ontgval  37434  sucneqond  38556  finxpreclem4  38585  finxpsuclem  38588  dfsuccl4  39672  suceldisj  40016  onexgt  44503  onepsuc  44515  ordnexbtwnsuc  44530  nlimsuc  44703  sucomisnotcard  44806