Theorem elelsuc 6385

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

Syntax hints:   → wi 4   ∨ wo 853   = wceq 1547   ∈ wcel 2119  suc csuc 6312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-sn 4556  df-suc 6316

This theorem is referenced by:  suctr  6398  pssnn  9093  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  pwsdompw  10116  fin1a2lem4  10316  grur1a  10733  bnj570  35087  fineqvnttrclselem3  35304  satom  35584  satfv0  35586  satfvsuc  35589  satf00  35602  satf0suc  35604  sat1el2xp  35607  fmla  35609  fmla0  35610  fmlasuc0  35612  satfdmfmla  35628  finxpsuclem  37759