Theorem elelsuc 6437

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1570   ∈ wcel 2145  suc csuc 6363

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-suc 6367

This theorem is used by:  suctr  6450  pssnn  9177  ttrcltr  9710  ttrclss  9714  ttrclselem2  9720  pwsdompw  10274  fin1a2lem4  10474  grur1a  10897  bnj570  35528  fineqvnttrclselem3  35774  satom  36100  satfv0  36102  satfvsuc  36105  satf00  36118  satf0suc  36120  sat1el2xp  36123  fmla  36125  fmla0  36126  fmlasuc0  36128  satfdmfmla  36144  nmulprop  36919  finxpsuclem  38300