Theorem elelsuc 6381

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1541   ∈ wcel 2111  suc csuc 6308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-sn 4574  df-suc 6312

This theorem is referenced by:  suctr  6394  pssnn  9078  ttrcltr  9606  ttrclss  9610  ttrclselem2  9616  pwsdompw  10094  fin1a2lem4  10294  grur1a  10710  bnj570  34917  fineqvnttrclselem3  35143  satom  35400  satfv0  35402  satfvsuc  35405  satf00  35418  satf0suc  35420  sat1el2xp  35423  fmla  35425  fmla0  35426  fmlasuc0  35428  satfdmfmla  35444  finxpsuclem  37441