Theorem elelsuc 6441

Description: Membership in a successor. (Contributed by NM, 20-Jun-1998.)

Assertion

Ref	Expression
elelsuc	⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵)

Proof of Theorem elelsuc

Step	Hyp	Ref	Expression
1		orc 881	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
2		elsucg 6436	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
3	1, 2	mpbird 260	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵)

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1569   ∈ wcel 2144  suc csuc 6367

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4150  df-sn 4585  df-suc 6371

This theorem is used by:  suctr  6454  pssnn  9191  ttrcltr  9724  ttrclss  9728  ttrclselem2  9734  pwsdompw  10288  fin1a2lem4  10488  grur1a  10911  bnj570  35585  fineqvnttrclselem3  35851  satom  36211  satfv0  36213  satfvsuc  36216  satf00  36229  satf0suc  36231  sat1el2xp  36234  fmla  36236  fmla0  36237  fmlasuc0  36239  satfdmfmla  36255  nmulprop  37035  finxpsuclem  38429  parswapprop  50885