Theorem elelsuc 6436

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

Syntax hints:   → wi 4   ∨ wo 860   = wceq 1570   ∈ wcel 2143  suc csuc 6362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-sn 4590  df-suc 6366

This theorem is referenced by:  suctr  6449  pssnn  9149  ttrcltr  9681  ttrclss  9685  ttrclselem2  9691  pwsdompw  10182  fin1a2lem4  10382  grur1a  10799  bnj570  35293  fineqvnttrclselem3  35536  satom  35848  satfv0  35850  satfvsuc  35853  satf00  35866  satf0suc  35868  sat1el2xp  35871  fmla  35873  fmla0  35874  fmlasuc0  35876  satfdmfmla  35892  nmulprop  36682  finxpsuclem  38043