Theorem elelsuc 6464

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-suc 6394

This theorem is used by:  suctr  6477  pssnn  9222  ttrcltr  9754  ttrclss  9758  ttrclselem2  9764  pwsdompw  10320  fin1a2lem4  10520  grur1a  10943  bnj570  35646  fineqvnttrclselem3  35932  satom  36329  satfv0  36331  satfvsuc  36334  satf00  36347  satf0suc  36349  sat1el2xp  36352  fmla  36354  fmla0  36355  fmlasuc0  36357  satfdmfmla  36373  nmulprop  37154  finxpsuclem  38588  parswapprop  51108