Theorem elelsuc 6468

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

Syntax hints:   → wi 4   ∨ wo 846   = wceq 1537   ∈ wcel 2108  suc csuc 6397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-suc 6401

This theorem is referenced by:  suctr  6481  pssnn  9234  ttrcltr  9785  ttrclss  9789  ttrclselem2  9795  pwsdompw  10272  fin1a2lem4  10472  grur1a  10888  bnj570  34881  satom  35324  satfv0  35326  satfvsuc  35329  satf00  35342  satf0suc  35344  sat1el2xp  35347  fmla  35349  fmla0  35350  fmlasuc0  35352  satfdmfmla  35368  finxpsuclem  37363