Theorem elelsuc 6421

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 878	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
2		elsucg 6416	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
3	1, 2	mpbird 259	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵)

Syntax hints:   → wi 4   ∨ wo 858   = wceq 1560   ∈ wcel 2142  suc csuc 6348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-sn 4583  df-suc 6352

This theorem is referenced by:  suctr  6434  pssnn  9137  ttrcltr  9671  ttrclss  9675  ttrclselem2  9681  pwsdompw  10159  fin1a2lem4  10360  grur1a  10777  bnj570  35197  fineqvnttrclselem3  35416  satom  35703  satfv0  35705  satfvsuc  35708  satf00  35721  satf0suc  35723  sat1el2xp  35726  fmla  35728  fmla0  35729  fmlasuc0  35731  satfdmfmla  35747  nmulprop  36537  finxpsuclem  37888